src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 58133 c7cc358a6972
parent 58131 1abeda3c3bc2
child 58137 feb69891e0fd
equal deleted inserted replaced
58132:6dcee1f6ea65 58133:c7cc358a6972
   173   #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy)
   173   #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy)
   174   handle ERROR _ => [];
   174   handle ERROR _ => [];
   175 
   175 
   176 fun get_all thy nesting_pref =
   176 fun get_all thy nesting_pref =
   177   let
   177   let
   178     val lthy = Named_Target.theory_init thy;
   178     val lthy = Proof_Context.init_global thy;
   179     val old_info_tab = Old_Datatype_Data.get_all thy;
   179     val old_info_tab = Old_Datatype_Data.get_all thy;
   180     val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
   180     val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
   181       |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
   181       |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
   182     val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names;
   182     val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names;
   183   in
   183   in