diff -r ffb5a181844b -r 8268b277d240 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Dec 28 19:51:25 2010 +0000
@@ -142,7 +142,7 @@
       val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
         Function_Common.default_config (pat_completeness_simp constr_thms) lthy
 
-      val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)
+      val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1)
       val {fs, simps, inducts, ...} = info
 
       val raw_bn_induct = (the inducts)
@@ -277,7 +277,7 @@
     val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
       Function_Common.default_config (pat_completeness_simp constr_thms) lthy
 
-    val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
+    val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy')
  
     val {fs, simps, inducts, ...} = info;
 
@@ -342,7 +342,7 @@
       val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
         Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy
     
-      val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy')
+      val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy')
 
       val {fs, simps, ...} = info;