# HG changeset patch # User ballarin # Date 1230038967 -3600 # Node ID 96b1b4d5157d1d5d88f17c0246e1abb1ea523dd5 # Parent 4dc278c8dc59a1f4e30422405ae76289a5f46219 More liberal consistency check for defines elements. diff -r 4dc278c8dc59 -r 96b1b4d5157d src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Dec 19 16:39:23 2008 +0100 +++ b/src/Pure/Isar/expression.ML Tue Dec 23 14:29:27 2008 +0100 @@ -486,11 +486,11 @@ val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in - exists (fn (x, _) => x = y) xs andalso - err "Attempt to define previously specified variable"; - exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso - err "Attempt to redefine variable"; - (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) + 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: