# HG changeset patch
# User wenzelm
# Date 1256066557 -7200
# Node ID 2f4b36efa95eaefb040702745e7a9b01de9e75a5
# Parent  2fefe039edf15ffd69bf2d6ea39064b0eb7d17ca
tuned;

diff -r 2fefe039edf1 -r 2f4b36efa95e src/HOL/Decision_Procs/Approximation.thy
--- 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"}
diff -r 2fefe039edf1 -r 2f4b36efa95e src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
--- 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
diff -r 2fefe039edf1 -r 2f4b36efa95e src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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