# HG changeset patch
# User wenzelm
# Date 1192803233 -7200
# Node ID 796190c7918d9eada31549ed59b21a9936f54e6d
# Parent  b8950f7cf92ed83429356a589ba11b75131e1316
do not export standard_infer_types;

diff -r b8950f7cf92e -r 796190c7918d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Oct 19 15:08:33 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Oct 19 16:13:53 2007 +0200
@@ -144,7 +144,6 @@
   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