# HG changeset patch
# User wenzelm
# Date 1137111180 -3600
# Node ID ad7ae7870427bafaa32b2c847d80992bbbe98b48
# Parent  8474756e4cbfa64663d85eca7acea21ddd5a5266
removed obsolete sign_of;

diff -r 8474756e4cbf -r ad7ae7870427 src/Pure/Isar/toplevel.ML
--- 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
diff -r 8474756e4cbf -r ad7ae7870427 src/Pure/codegen.ML
--- 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 =