--- a/Nominal/NewParser.thy	Tue Aug 17 18:17:53 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 18 00:19:15 2010 +0800
@@ -226,7 +226,7 @@
 *}
 
 ML {*
-fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
+fun define_raw_dts dts bn_funs bn_eqs binds lthy =
 let
   val thy = ProofContext.theory_of lthy
   val thy_name = Context.theory_name thy
@@ -261,7 +261,8 @@
 *}
 
 ML {*
-fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy =
+(* should be in nominal_dt_rawfuns *)
+fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
   if null raw_bn_funs 
   then ([], [], [], [], lthy)
   else 
@@ -269,8 +270,8 @@
       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 (Local_Theory.restore lthy1)
-      val {fs, simps, inducts, ...} = info;
+      val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)
+      val {fs, simps, inducts, ...} = info
 
       val raw_bn_induct = (the inducts)
       val raw_bn_eqs = the simps
@@ -301,7 +302,7 @@
   val _ = warning "Definition of raw datatypes";
   val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
     if get_STEPS lthy > 0 
-    then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+    then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
@@ -339,14 +340,14 @@
   val _ = warning "Definition of raw fv-functions";
   val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
-    then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
-      (raw_inject_thms @ raw_distinct_thms) lthy3
+    then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
+      (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
     if get_STEPS lthy3a > 3 
     then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
-      (raw_inject_thms @ raw_distinct_thms) lthy3a
+      (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
     else raise TEST lthy3a
 
   (* definition of raw alphas *)