diff -r 66f44de8bf5b -r e16523f01908 Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Sat Dec 12 02:01:33 2009 +0100
+++ b/Quot/Examples/LFex.thy	Sat Dec 12 13:53:46 2009 +0100
@@ -259,7 +259,7 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
-done
+ done
 
 (* Does not work:
 lemma