--- a/Nominal/NewParser.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/NewParser.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -251,7 +251,7 @@
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
 
-val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0);
+val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100);
 
 fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
@@ -259,7 +259,7 @@
 setup STEPS_setup
 
 ML {*
-fun nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses lthy =
+fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
   val _ = warning "Definition of raw datatypes";
@@ -437,7 +437,6 @@
   val qty_full_names = map (fst o dest_Type) qtys
   val qty_names = map Long_Name.base_name qty_full_names             
 
-
   (* defining of quotient term-constructors, binding functions, free vars functions *)
   val _ = warning "Defining the quotient constants"
   val qconstrs_descr = 
@@ -517,24 +516,24 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
-  
-  (* temporary theorem bindings *)
+  (* noting the theorems *)  
+
+  (* generating the prefix for the theorem names *)
+  val thms_name = 
+    the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
+  fun thms_suffix s = Binding.qualified true s thms_name 
+
   val (_, lthy9') = lthyB
-     |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts) 
-     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs)
-     ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs) 
-     ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs) 
-     ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps) 
-     ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts) 
-     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt)
-     ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct]) 
-     ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts)
+     |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
+     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
+     ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
+     ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
+     ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) 
+     ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
+     ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
+     ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
+     ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      
-
-  val _ = 
-    if get_STEPS lthy > 21
-    then true else raise TEST lthy9'
-  
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
@@ -692,11 +691,10 @@
 *}
 
 ML {*
-fun nominal_datatype2_cmd (opt_thm_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
+fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
 let
-  val (pre_typ_names, pre_typs) = split_list
-    (map (fn (tvs, tname, mx, _) =>
-      (Binding.name_of tname, (tname, length tvs, mx))) dt_strs)
+  val pre_typs = 
+    map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs
 
   (* this theory is used just for parsing *)
   val thy = ProofContext.theory_of lthy  
@@ -710,10 +708,8 @@
     ||>> prepare_bclauses dt_strs 
 
   val bclauses' = complete dt_strs bclauses
-  val thm_name = 
-    the_default (Binding.name (space_implode "_" pre_typ_names)) opt_thm_name 
 in
-  timeit (fn () => nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd)
+  timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd)
 end
 *}