--- 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