src/Pure/Isar/obtain.ML
changeset 16787 b6b6e2faaa41
parent 16606 e45c9a95a554
child 16842 5979c46853d1
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Jul 13 10:48:21 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jul 13 11:16:34 2005 +0200
     1.3 @@ -89,8 +89,8 @@
     1.4      val bound_thesis_raw as (bound_thesis_name, _) =
     1.5        Term.dest_Free (bind_thesis (Free (thesisN, propT)));
     1.6      val bound_thesis_var =
     1.7 -      foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
     1.8 -        | (v, t) => v) (bound_thesis_raw, bound_thesis);
     1.9 +      fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v)
    1.10 +        | _ => I) bound_thesis bound_thesis_raw;
    1.11  
    1.12      fun occs_var x = Library.get_first (fn t =>
    1.13        ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;