# 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: