More liberal consistency check for defines elements.

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