# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260622426 -3600
# Node ID e16523f01908fe7e2d74d745dcb4de396f1e247d
# Parent  66f44de8bf5be6760fad5e4469c9e4d55265ad57
trivial

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