--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon May 03 14:25:56 2010 +0200
@@ -129,7 +129,7 @@
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 []
@@ -153,7 +153,7 @@
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))
@@ -188,7 +188,7 @@
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