--- a/src/HOL/Decision_Procs/Approximation.thy Tue Oct 20 20:54:31 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Oct 20 21:22:37 2009 +0200
@@ -3462,9 +3462,9 @@
fun approx_form prec ctxt t =
realify t
- |> prepare_form (Context.theory_of_proof ctxt)
+ |> prepare_form (ProofContext.theory_of ctxt)
|> (fn arith_term =>
- reify_form (Context.theory_of_proof ctxt) arith_term
+ reify_form (ProofContext.theory_of ctxt) arith_term
|> HOLogic.dest_Trueprop |> dest_interpret_form
|> (fn (data, xs) =>
mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
--- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Oct 20 20:54:31 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Oct 20 21:22:37 2009 +0200
@@ -97,7 +97,7 @@
val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
- (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k))
+ (fn (x, k) => (cterm_of (ProofContext.theory_of ctxt) (Free (x, @{typ real})), k))
fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
List.foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Oct 20 20:54:31 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Oct 20 21:22:37 2009 +0200
@@ -613,7 +613,7 @@
(* TODO: interim: this is probably not right.
What we want is mapping onto simple PGIP name/context model. *)
val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
- val thy = Context.theory_of_proof ctx
+ val thy = ProofContext.theory_of ctx
val ths = [PureThy.get_thm thy thmname]
val deps = #2 (thms_deps ths);
in