1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 20:21:59 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 23:01:23 2014 +0200
     1.3 @@ -228,6 +228,9 @@
     1.4      map (Term.subst_TVars rho) ts0
     1.5    end;
     1.6  
     1.7 +fun mk_set Ts t =
     1.8 +  subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
     1.9 +
    1.10  fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
    1.11    | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
    1.12    | unzip_recT _ T = [T];
    1.13 @@ -528,7 +531,7 @@
    1.14  
    1.15      val us = map2 (curry Free) us' fpTs;
    1.16  
    1.17 -    fun mk_sets_nested bnf =
    1.18 +    fun mk_sets bnf =
    1.19        let
    1.20          val Type (T_name, Us) = T_of_bnf bnf;
    1.21          val lives = lives_of_bnf bnf;
    1.22 @@ -541,19 +544,14 @@
    1.23          (T_name, map mk_set Us)
    1.24        end;
    1.25  
    1.26 -    val setss_nested = map mk_sets_nested fp_nesting_bnfs;
    1.27 +    val setss_fp_nesting = map mk_sets fp_nesting_bnfs;
    1.28  
    1.29      val (induct_thms, induct_thm) =
    1.30        let
    1.31 -        fun mk_set Ts t =
    1.32 -          let val Type (_, Ts0) = domain_type (fastype_of t) in
    1.33 -            Term.subst_atomic_types (Ts0 ~~ Ts) t
    1.34 -          end;
    1.35 -
    1.36          fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) =
    1.37              [([], (find_index (curry (op =) X) Xs + 1, x))]
    1.38            | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) =
    1.39 -            (case AList.lookup (op =) setss_nested T_name of
    1.40 +            (case AList.lookup (op =) setss_fp_nesting T_name of
    1.41                NONE => []
    1.42              | SOME raw_sets0 =>
    1.43                let
    1.44 @@ -1298,9 +1296,6 @@
    1.45                val set_thmss = map mk_set_thms fp_set_thms;
    1.46                val set_thms = flat set_thmss;
    1.47  
    1.48 -              fun mk_set Ts t =
    1.49 -                subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
    1.50 -
    1.51                val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
    1.52  
    1.53                val set_empty_thms =