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