warn_extra_tfrees;

--- a/src/Pure/Isar/obtain.ML	Fri Oct 22 20:25:19 1999 +0200
+++ b/src/Pure/Isar/obtain.ML	Fri Oct 22 21:48:50 1999 +0200
@@ -84,6 +84,7 @@
 
     val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
     val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
+    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     fun find_free x t =
       (case Proof.find_free t x of Some (Free a) => Some a | _ => None);