src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

     val res = Name.names ctxt s xs
   in (res, fold Name.declare (map fst res) ctxt) end
   
 fun split_all_pairs thy th =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val ((_, [th']), ctxt') = Variable.import true [th] ctxt
     val t = prop_of th'
     val frees = Term.add_frees t [] 
     val freenames = Term.add_free_names t []
     val nctxt = Name.make_context freenames

   end;
 
 
 fun inline_equations thy th =
   let
-    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy)
+    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init_global thy)
     val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
     (*val _ = print_step options 
       ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
        ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
        ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)

     val t = Const (AxClass.unoverload_const thy (c, T), T)*)
     val _ = if show_steps options then
         tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
           " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
       else ()
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     fun filtering th =
       if is_equationlike th andalso
         defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
         SOME (normalize_equation thy th)
       else