warn_extra_tfrees;
authorwenzelm
Fri Oct 22 21:48:50 1999 +0200 (1999-10-22)
changeset 7923895d31b54da5
parent 7922 b284079cd902
child 7924 5fee69b1f5fe
warn_extra_tfrees;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Oct 22 20:25:19 1999 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Fri Oct 22 21:48:50 1999 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4  
     1.5      val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
     1.6      val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
     1.7 +    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
     1.8  
     1.9      fun find_free x t =
    1.10        (case Proof.find_free t x of Some (Free a) => Some a | _ => None);