# 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