diff -r f1980f89c405 -r 83990a42a068 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 18:00:55 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 18:17:53 2010 +0800
@@ -21,7 +21,9 @@
 where
   "bn (As x y t) = {atom x}"
 
-(* can lift *)
+ML {* Function.prove_termination *}
+
+text {* can lift *}
 
 thm distinct
 thm trm_raw_assg_raw.inducts