tuned code

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 20:21:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 23:01:23 2014 +0200
@@ -228,6 +228,9 @@
     map (Term.subst_TVars rho) ts0
   end;
 
+fun mk_set Ts t =
+  subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+
 fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
   | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
   | unzip_recT _ T = [T];
@@ -528,7 +531,7 @@
 
     val us = map2 (curry Free) us' fpTs;
 
-    fun mk_sets_nested bnf =
+    fun mk_sets bnf =
       let
         val Type (T_name, Us) = T_of_bnf bnf;
         val lives = lives_of_bnf bnf;
@@ -541,19 +544,14 @@
         (T_name, map mk_set Us)
       end;
 
-    val setss_nested = map mk_sets_nested fp_nesting_bnfs;
+    val setss_fp_nesting = map mk_sets fp_nesting_bnfs;
 
     val (induct_thms, induct_thm) =
       let
-        fun mk_set Ts t =
-          let val Type (_, Ts0) = domain_type (fastype_of t) in
-            Term.subst_atomic_types (Ts0 ~~ Ts) t
-          end;
-
         fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) =
             [([], (find_index (curry (op =) X) Xs + 1, x))]
           | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) =
-            (case AList.lookup (op =) setss_nested T_name of
+            (case AList.lookup (op =) setss_fp_nesting T_name of
               NONE => []
             | SOME raw_sets0 =>
               let
@@ -1298,9 +1296,6 @@
               val set_thmss = map mk_set_thms fp_set_thms;
               val set_thms = flat set_thmss;
 
-              fun mk_set Ts t =
-                subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
-
               val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
 
               val set_empty_thms =