--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Mar 06 23:52:35 2015 +0100
@@ -181,7 +181,7 @@
(** parser context **)
-val not_false = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
+val not_false = Thm.cterm_of @{context} (@{const Not} $ @{const False})
fun make_context ctxt typs terms =
let
@@ -381,7 +381,7 @@
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
-val ctrue = Thm.global_cterm_of @{theory} @{const True}
+val ctrue = Thm.cterm_of @{context} @{const True}
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
(the o mk_fun (K (SOME ctrue)))) st