# HG changeset patch
# User haftmann
# Date 1279627266 -7200
# Node ID d1ddd0269baee7e4fd8a46c11d31dfa5b98e78a8
# Parent  b22db9ecf416bd4b466ba5f003e1daf504aba131
accomodate for scope of "as" binding in ML

diff -r b22db9ecf416 -r d1ddd0269bae src/HOL/Tools/abel_cancel.ML
--- 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 =