--- a/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 18:17:53 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Wed Aug 18 00:19:15 2010 +0800
@@ -25,7 +25,7 @@
   val listify: Proof.context -> term -> term
 
   val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
-    thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
+    thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
  
   val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
 end
@@ -210,7 +210,7 @@
   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 
-fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms lthy =
+fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy =
 let
   val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
@@ -233,19 +233,18 @@
 
   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 (Local_Theory.restore lthy')
-
+  
+  val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
+ 
   val {fs, simps, inducts, ...} = info;
 
   val morphism = ProofContext.export_morphism lthy'' lthy
   val fs_exp = map (Morphism.term morphism) fs
   val simps_exp = map (Morphism.thm morphism) (the simps)
   val inducts_exp = map (Morphism.thm morphism) (the inducts)
-  val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
-  
+  val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
 in
-  (fv_frees_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
+  (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
 end