author | blanchet |
Mon, 01 Sep 2014 19:58:25 +0200 | |
changeset 58133 | c7cc358a6972 |
parent 58132 | 6dcee1f6ea65 |
child 58134 | b563ec62d04e |
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 19:57:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 19:58:25 2014 +0200 @@ -175,7 +175,7 @@ fun get_all thy nesting_pref = let - val lthy = Named_Target.theory_init thy; + val lthy = Proof_Context.init_global thy; val old_info_tab = Old_Datatype_Data.get_all thy; val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));