removed obsolete sign_of;
authorwenzelm
Sat, 05 Aug 2006 14:52:55 +0200
changeset 20341 41e77e688886
parent 20340 6afc1c133b86
child 20342 4392003fcbfa
removed obsolete sign_of;
src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Aug 05 14:52:53 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Aug 05 14:52:55 2006 +0200
@@ -16,7 +16,6 @@
   val assert_bottom: bool -> state -> state
   val context_of: state -> context
   val theory_of: state -> theory
-  val sign_of: state -> theory    (*obsolete*)
   val map_context: (context -> context) -> state -> state
   val add_binds_i: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
@@ -195,7 +194,6 @@
 
 val context_of = #context o current;
 val theory_of = ProofContext.theory_of o context_of;
-val sign_of = theory_of;
 
 fun map_context f =
   map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));