added find_free (from term.ML);
authorwenzelm
Tue Jul 25 21:18:08 2006 +0200 (2006-07-25)
changeset 2020124b49cbd438b
parent 20200 c6fb50dbbc30
child 20202 87205ea2af06
added find_free (from term.ML);
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Jul 25 21:18:07 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jul 25 21:18:08 2006 +0200
     1.3 @@ -99,6 +99,13 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun find_free t x =
     1.8 +  let
     1.9 +    exception Found of term;
    1.10 +    fun find (t as Free (x', _)) = if x = x' then raise Found t else I
    1.11 +      | find _ = I;
    1.12 +  in (fold_aterms find t (); NONE) handle Found v => SOME v end;
    1.13 +
    1.14  fun gen_obtain prep_att prep_vars prep_propp
    1.15      name raw_vars raw_asms int state =
    1.16    let
    1.17 @@ -124,7 +131,7 @@
    1.18      val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
    1.19  
    1.20      fun occs_var x = Library.get_first (fn t =>
    1.21 -      Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.22 +      find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.23      val parms =
    1.24        map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs);
    1.25