# HG changeset patch
# User blanchet
# Date 1473257219 -7200
# Node ID 42b98ab11598add6091f191306b3f2d7106f8866
# Parent  9cd3dabfeea8539b7578b6806ee9d29521922f81
tuning

diff -r 9cd3dabfeea8 -r 42b98ab11598 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 13:53:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 16:06:59 2016 +0200
@@ -2140,9 +2140,9 @@
   end;
 
 fun define_co_datatypes prepare_plugins prepare_constraint prepare_typ prepare_term fp construct_fp
-    ((raw_plugins, discs_sels0), specs) no_defs_lthy =
+    ((raw_plugins, discs_sels0), specs) lthy =
   let
-    val plugins = prepare_plugins no_defs_lthy raw_plugins;
+    val plugins = prepare_plugins lthy raw_plugins;
     val discs_sels = discs_sels0 orelse fp = Greatest_FP;
 
     val nn = length specs;
@@ -2154,8 +2154,8 @@
     val pred_bs = map pred_binding_of_spec specs;
 
     fun prepare_type_arg (_, (ty, c)) =
-      let val TFree (s, _) = prepare_typ no_defs_lthy ty in
-        TFree (s, prepare_constraint no_defs_lthy c)
+      let val TFree (s, _) = prepare_typ lthy ty in
+        TFree (s, prepare_constraint lthy c)
       end;
 
     val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
@@ -2170,7 +2170,7 @@
       Typedecl.basic_typedecl {final = true}
         (type_binding_of_spec spec, num_As, Mixfix.reset_pos (mixfix_of_spec spec));
 
-    val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy;
+    val (fake_T_names, fake_lthy) = fold_map add_fake_type specs lthy;
 
     val qsoty = quote o Syntax.string_of_typ fake_lthy;
 
@@ -2179,7 +2179,7 @@
           "datatype specification"));
 
     val bad_args =
-      map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy))) unsorted_As
+      map (Logic.type_map (singleton (Variable.polymorphic lthy))) unsorted_As
       |> filter_out Term.is_TVar;
     val _ = null bad_args orelse
       error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^
@@ -2215,7 +2215,7 @@
 
     val fake_Ts = map (fn s => Type (s, As)) fake_T_names;
 
-    val ((((Bs0, Cs), Es), Xs), _) = no_defs_lthy
+    val ((((Bs0, Cs), Es), Xs), _) = lthy
       |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
       |> mk_TFrees num_As
       ||>> mk_TFrees nn
@@ -2277,7 +2277,7 @@
            lthy)) =
       fixpoint_bnf false I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
         (map dest_TFree As) (map dest_TFree killed_As) (map dest_TFree Xs) ctrXs_repTs
-        empty_comp_cache no_defs_lthy
+        empty_comp_cache lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
           Type (bad_tc, _) =>
@@ -2289,11 +2289,10 @@
               quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
               \it";
           in
-            if is_some (bnf_of no_defs_lthy bad_tc) orelse
-               is_some (fp_sugar_of no_defs_lthy bad_tc) then
+            if is_some (bnf_of lthy bad_tc) orelse is_some (fp_sugar_of lthy bad_tc) then
               error ("Inadmissible " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
                 " in type expression " ^ fake_T_backdrop)
-            else if is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
+            else if is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy)
                 bad_tc) then
               error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
                 " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^
@@ -2353,7 +2352,9 @@
     val code_attrs =
       if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
 
-    val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
+    val real_unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fpTs);
+
+    val ctr_Tsss = map (map (map real_unfreeze_fp)) ctrXs_Tsss;
     val ns = map length ctr_Tsss;
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
@@ -2364,25 +2365,27 @@
     fun define_ctrs_dtrs_for_type_etc fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
         ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
         abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss
-        raw_sel_default_eqs no_defs_lthy =
+        raw_sel_default_eqs lthy =
       let
         val fp_b_name = Binding.name_of fp_b;
 
         val ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy) =
           define_ctrs_dtrs_for_type fp_b_name fpT ctor dtor ctor_dtor dtor_ctor n ks abs
-            ctr_bindings ctr_mixfixes ctr_Tss no_defs_lthy;
+            ctr_bindings ctr_mixfixes ctr_Tss lthy;
 
         val ctrs = map (mk_ctr As) ctrs0;
 
-        val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss;
-        val sel_bTs =
-          flat sel_bindingss ~~ flat sel_Tss
-          |> filter_out (Binding.is_empty o fst)
-          |> distinct (Binding.eq_name o apply2 fst);
-
-        val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
-
-        val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
+        val sel_default_eqs =
+          let
+            val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss;
+            val sel_bTs =
+              flat sel_bindingss ~~ flat sel_Tss
+              |> filter_out (Binding.is_empty o fst)
+              |> distinct (Binding.eq_name o apply2 fst);
+            val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy
+          in
+            map (prepare_term sel_default_lthy) raw_sel_default_eqs
+          end;
 
         fun mk_binding pre =
           Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);