# 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));