--- 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