# HG changeset patch # User haftmann # Date 1192569177 -7200 # Node ID 8e702c7adc349c302513b3520394a5eb0109d356 # Parent af5ef0d4d6553abce361b461f23ecad6bbb99f2b exported standard_term_check diff -r af5ef0d4d655 -r 8e702c7adc34 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Oct 16 23:12:45 2007 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Oct 16 23:12:57 2007 +0200 @@ -144,6 +144,7 @@ val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> Markup.property list -> bstring * term -> Proof.context -> (term * term) * Proof.context + val standard_infer_types: Proof.context -> term list -> term list val revert_abbrev: string -> string -> Proof.context -> Proof.context val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b