# HG changeset patch
# User wenzelm
# Date 1154782375 -7200
# Node ID 41e77e688886f2c7babf6916d14f4dc8f3aa10d6
# Parent  6afc1c133b8668a01cd565643d879fee8c90746d
removed obsolete sign_of;

diff -r 6afc1c133b86 -r 41e77e688886 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));