# HG changeset patch
# User wenzelm
# Date 940621730 -7200
# Node ID 895d31b54da512dfe5c33caacda28ee1b895e249
# Parent  b284079cd902b753a37a701b9a082bc2f699d277
warn_extra_tfrees;

diff -r b284079cd902 -r 895d31b54da5 src/Pure/Isar/obtain.ML
--- 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);