src/Pure/Isar/expression.ML
changeset 49749 f27c96e98672
parent 47315 89a4bbf9790d
child 49817 85b37aece3b3
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Oct 09 20:05:17 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Oct 09 20:23:58 2012 +0200
     1.3 @@ -527,11 +527,11 @@
     1.4      val b' = norm_term env b;
     1.5      fun err msg = error (msg ^ ": " ^ quote y);
     1.6    in
     1.7 -    case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
     1.8 -      [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) |
     1.9 -      dups => if forall (fn (_, b'') => b' aconv b'') dups
    1.10 -        then (xs, env, eqs)
    1.11 -        else err "Attempt to redefine variable"
    1.12 +    (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
    1.13 +      [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
    1.14 +    | dups =>
    1.15 +        if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
    1.16 +        else err "Attempt to redefine variable")
    1.17    end;
    1.18  
    1.19  (* text has the following structure: