diff -r d7e8b9b78e28 -r ddb69d9f45d0 Nominal/Ex/LetSimple2.thy
--- a/Nominal/Ex/LetSimple2.thy	Fri Jul 15 22:48:37 2011 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Sat Jul 16 21:36:43 2011 +0100
@@ -1,19 +1,7 @@
-theory Let
+theory LetSimple2
 imports "../Nominal2" 
 begin
 
-(*
-ML {*
-   val lemma =
-     Term_XML.Encode.term #>
-     YXML.string_of_body #>
-     translate_string (fn c => if ord c < 10 then "\\00" ^ string_of_int (ord c) else c) #>
-     quote #> prefix "lemma " #>
-     Markup.markup Markup.sendback #> writeln
-*}
-
-ML {* lemma @{prop "x == x"} *}
-*)
 
 atom_decl name