--- a/src/Pure/Isar/toplevel.ML Fri Jan 13 01:12:59 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Jan 13 01:13:00 2006 +0100
@@ -23,7 +23,6 @@
val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
val context_of: state -> Context.generic
val theory_of: state -> theory
- val sign_of: state -> theory (*obsolete*)
val body_context_of: state -> Proof.context
val proof_of: state -> Proof.state
val proof_position_of: state -> int
@@ -166,7 +165,6 @@
val context_of = node_case Context.Theory (Context.Proof o Proof.context_of);
val theory_of = node_case I Proof.theory_of;
-val sign_of = theory_of;
fun body_context_of state =
(case node_of state of
--- a/src/Pure/codegen.ML Fri Jan 13 01:12:59 2006 +0100
+++ b/src/Pure/codegen.ML Fri Jan 13 01:13:00 2006 +0100
@@ -1195,7 +1195,7 @@
|| parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
(fn (ps, g) => Toplevel.keep (fn st =>
test_goal (app (getOpt (Option.map
- (map (fn f => f (Toplevel.sign_of st))) ps, []))
+ (map (fn f => f (Toplevel.theory_of st))) ps, []))
(get_test_params (Toplevel.theory_of st), [])) g st)));
val valueP =