# HG changeset patch
# User wenzelm
# Date 1344268445 -7200
# Node ID 538ea0adb8e109b7d8c27dfe2a5cafc473c61af8
# Parent  db82a65cdb8018908ebe9e4032e43d4c50fe32bf# Parent  ceeea46bdeba4eb3e5eebd00b549e4ba41ceeef2
merged

diff -r ceeea46bdeba -r 538ea0adb8e1 Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Mon Aug 06 16:05:29 2012 +0200
+++ b/Admin/MacOS/App1/script	Mon Aug 06 17:54:05 2012 +0200
@@ -48,9 +48,9 @@
 # Proof General / Emacs
 
 PROOFGENERAL_EMACS="$(choosefrom \
-  "$THIS/Emacs.app/Contents/MacOS/Emacs" \
-  "$SUPER_APP/Emacs.app/Contents/MacOS/Emacs" \
-  /Applications/Emacs.app/Contents/MacOS/Emacs \
+  "$THIS/Aquamacs.app/Contents/MacOS/Aquamacs" \
+  "$SUPER_APP/Aquamacs.app/Contents/MacOS/Aquamacs" \
+  /Applications/Aquamacs.app/Contents/MacOS/Aquamacs \
   "")"
 
 declare -a EMACS_OPTIONS=()
diff -r ceeea46bdeba -r 538ea0adb8e1 src/HOL/Tools/group_cancel.ML
--- a/src/HOL/Tools/group_cancel.ML	Mon Aug 06 16:05:29 2012 +0200
+++ b/src/HOL/Tools/group_cancel.ML	Mon Aug 06 17:54:05 2012 +0200
@@ -49,16 +49,14 @@
 
 val coeff_ord = prod_ord bool_ord Term_Ord.term_ord
 
-exception Cancel
-
-fun find_common ord xs ys =
+fun find_all_common ord xs ys =
   let
     fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
         (case ord (x, y) of
-          EQUAL => (px, py)
+          EQUAL => (px, py) :: find xs' ys'
         | LESS => find xs' ys
         | GREATER => find xs ys')
-      | find _ _ = raise Cancel
+      | find _ _ = []
     fun ord' ((x, _), (y, _)) = ord (x, y)
   in
     find (sort ord' xs) (sort ord' ys)
@@ -66,14 +64,20 @@
 
 fun cancel_conv rule ct =
   let
+    fun cancel1_conv (lpath, rpath) =
+      let
+        val lconv = move_to_front lpath
+        val rconv = move_to_front rpath
+        val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
+      in
+        conv1 then_conv Conv.rewr_conv rule
+      end
     val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
-    val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs)
-    val lconv = move_to_front lpath
-    val rconv = move_to_front rpath
-    val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
-    val conv = conv1 then_conv Conv.rewr_conv rule
+    val common = find_all_common coeff_ord (atoms lhs) (atoms rhs)
+    val conv =
+      if null common then Conv.no_conv
+      else Conv.every_conv (map cancel1_conv common)
   in conv ct end
-    handle Cancel => raise CTERM ("no_conversion", [])
 
 val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left})
 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})