src/Pure/Isar/expression.ML
changeset 42482 42c7ef050bc3
parent 42440 5e7a7343ab11
child 42494 eef1a23c9077
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 26 22:22:39 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Apr 27 10:31:18 2011 +0200
     1.3 @@ -380,12 +380,10 @@
     1.4      val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
     1.5      val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
     1.6  
     1.7 -    val add_free = fold_aterms
     1.8 -      (fn Free (x, T) => not (Variable.is_fixed ctxt3 x) ? insert (op =) (x, T) | _ => I);
     1.9      val _ =
    1.10        if fixed_frees then ()
    1.11        else
    1.12 -        (case fold (fold add_free o snd o snd) insts' [] of
    1.13 +        (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of
    1.14            [] => ()
    1.15          | frees => error ("Illegal free variables in expression: " ^
    1.16              commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));