Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 09 Oct 2012 20:23:58 +0200
changeset 49749 f27c96e98672
parent 49748 a346daa8a1f4
child 49750 444cfaa331c9
tuned;
src/Pure/Isar/expression.ML file | annotate | diff | comparison | revisions 
--- 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:
isabelle