src/Pure/Isar/obtain.ML
changeset 7923 895d31b54da5
parent 7677 de2e468a42c8
child 8094 62b45a2e6ecb
     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);