# HG changeset patch
# User blanchet
# Date 1377708290 -7200
# Node ID 67e122cedbba88b9d0bcb2f38c955b8799d9a309
# Parent  daa550823c9f562eac0807ecbd04755ee6353e9b
tuning

diff -r daa550823c9f -r 67e122cedbba src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 17:11:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 18:44:50 2013 +0200
@@ -1119,8 +1119,8 @@
            xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
            dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
            lthy)) =
-      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
-        no_defs_lthy0;
+      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
+        fake_Ts fp_eqs no_defs_lthy0;
 
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
diff -r daa550823c9f -r 67e122cedbba src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Wed Aug 28 17:11:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Wed Aug 28 18:44:50 2013 +0200
@@ -571,18 +571,18 @@
     |> unfold_thms ctxt unfolds
   end;
 
-fun fp_bnf construct_fp bs resBs eqs lthy =
+fun fp_bnf construct_fp bs resBs fp_eqs lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
-    val (lhss, rhss) = split_list eqs;
+    val (lhss, rhss) = split_list fp_eqs;
 
     (* FIXME: because of "@ lhss", the output could contain type variables that are not in the
        input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
     fun fp_sort Ass =
       subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss;
 
-    val name = mk_common_name (map Binding.name_of bs);
+    val common_name = mk_common_name (map Binding.name_of bs);
 
     fun raw_qualify b =
       let val s = Binding.name_of b in
@@ -594,7 +594,7 @@
         (empty_unfolds, lthy));
 
     fun qualify i =
-      let val namei = name ^ nonzero_string_of_int i;
+      let val namei = common_name ^ nonzero_string_of_int i;
       in Binding.qualify true namei end;
 
     val Ass = map (map dest_TFree) livess;