# HG changeset patch
# User blanchet
# Date 1409594305 -7200
# Node ID c7cc358a6972fea0ef62f67297f0337fd4b8cdcb
# Parent  6dcee1f6ea6531f03bd4bd2a8f986c49793175ea
avoid more 'bad background theory' issues

diff -r 6dcee1f6ea65 -r c7cc358a6972 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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));