# HG changeset patch # User wenzelm # Date 1349807038 -7200 # Node ID f27c96e9867262c6aac840fea22edb842fafaf26 # Parent a346daa8a1f4f66aec8f99ae72172bd3c79d2412 tuned; diff -r a346daa8a1f4 -r f27c96e98672 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Oct 09 20:05:17 2012 +0200 +++ b/src/Pure/Isar/expression.ML Tue Oct 09 20:23:58 2012 +0200 @@ -527,11 +527,11 @@ val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in - case filter (fn (Free (y', _), _) => y = y' | _ => false) env of - [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) | - dups => if forall (fn (_, b'') => b' aconv b'') dups - then (xs, env, eqs) - else err "Attempt to redefine variable" + (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of + [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) + | dups => + if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs) + else err "Attempt to redefine variable") end; (* text has the following structure: