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.
accomodate for scope of "as" binding in ML
authorhaftmann
Tue, 20 Jul 2010 14:01:06 +0200
changeset 37895 d1ddd0269bae
parent 37894 b22db9ecf416
child 37896 4274a8d60fa1
accomodate for scope of "as" binding in ML
src/HOL/Tools/abel_cancel.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/abel_cancel.ML	Tue Jul 20 10:24:18 2010 +0200
+++ b/src/HOL/Tools/abel_cancel.ML	Tue Jul 20 14:01:06 2010 +0200
@@ -28,16 +28,16 @@
 
 fun atoms fml = add_atoms true fml [];
 
-fun zero1 pt (c as Const (@{const_name Groups.plus}, _) $ x $ y) =
+fun zero1 pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) =
       (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
-                                   | SOME z => SOME(c $ x $ z))
+                                   | SOME z => SOME (c $ x $ z))
        | SOME z => SOME (c $ z $ y))
-  | zero1 pt (c as Const (@{const_name Groups.minus}, _) $ x $ y) =
+  | zero1 pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) =
       (case zero1 pt x of
          NONE => (case zero1 (apfst not pt) y of NONE => NONE
                   | SOME z => SOME (c $ x $ z))
        | SOME z => SOME (c $ z $ y))
-  | zero1 pt (c as Const (@{const_name Groups.uminus}, _) $ x) =
+  | zero1 pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) =
       (case zero1 (apfst not pt) x of NONE => NONE
        | SOME z => SOME (c $ z))
   | zero1 (pos, t) u =
isabelle