# HG changeset patch
# User wenzelm
# Date 1169208577 -3600
# Node ID d9b614dc883d751874de82047e38f2f1bbca9cbf
# Parent  4c53bb6e10e45dfca5308a7cbfde3b994eaa85ef
added generic_theory_of;
adapted ML context operations;

diff -r 4c53bb6e10e4 -r d9b614dc883d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Jan 19 13:09:36 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Jan 19 13:09:37 2007 +0100
@@ -23,6 +23,7 @@
   val node_of: state -> node
   val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
   val context_of: state -> Proof.context
+  val generic_theory_of: state -> generic_theory
   val theory_of: state -> theory
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
@@ -194,6 +195,7 @@
 fun node_case f g state = cases_node f g (node_of state);
 
 val context_of = node_case Context.proof_of Proof.context_of;
+val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
 val theory_of = node_case Context.theory_of Proof.theory_of;
 val proof_of = node_case (fn _ => raise UNDEF) I;
 
@@ -266,7 +268,7 @@
 
 fun with_context f xs =
   (case Context.get_context () of NONE => []
-  | SOME thy => map (f thy) xs);
+  | SOME context => map (f (Context.proof_of context)) xs);
 
 fun raised name [] = "exception " ^ name ^ " raised"
   | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
@@ -292,12 +294,13 @@
       raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
   | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
   | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
-        with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
+        with_context ProofContext.string_of_typ Ts @ with_context ProofContext.string_of_term ts)
   | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
-  | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
+  | exn_msg true (TERM (msg, ts)) =
+      raised "TERM" (msg :: with_context ProofContext.string_of_term ts)
   | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
   | exn_msg true (THM (msg, i, thms)) =
-      raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
+      raised ("THM " ^ string_of_int i) (msg :: with_context ProofContext.string_of_thm thms)
   | exn_msg _ Option.Option = raised "Option" []
   | exn_msg _ Library.UnequalLengths = raised "UnequalLengths" []
   | exn_msg _ Empty = raised "Empty" []