1.1 --- a/src/HOL/Tools/group_cancel.ML	Mon Aug 06 14:33:23 2012 +0200
     1.2 +++ b/src/HOL/Tools/group_cancel.ML	Mon Aug 06 15:12:18 2012 +0200
     1.3 @@ -49,16 +49,14 @@
     1.4  
     1.5  val coeff_ord = prod_ord bool_ord Term_Ord.term_ord
     1.6  
     1.7 -exception Cancel
     1.8 -
     1.9 -fun find_common ord xs ys =
    1.10 +fun find_all_common ord xs ys =
    1.11    let
    1.12      fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    1.13          (case ord (x, y) of
    1.14 -          EQUAL => (px, py)
    1.15 +          EQUAL => (px, py) :: find xs' ys'
    1.16          | LESS => find xs' ys
    1.17          | GREATER => find xs ys')
    1.18 -      | find _ _ = raise Cancel
    1.19 +      | find _ _ = []
    1.20      fun ord' ((x, _), (y, _)) = ord (x, y)
    1.21    in
    1.22      find (sort ord' xs) (sort ord' ys)
    1.23 @@ -66,14 +64,20 @@
    1.24  
    1.25  fun cancel_conv rule ct =
    1.26    let
    1.27 +    fun cancel1_conv (lpath, rpath) =
    1.28 +      let
    1.29 +        val lconv = move_to_front lpath
    1.30 +        val rconv = move_to_front rpath
    1.31 +        val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    1.32 +      in
    1.33 +        conv1 then_conv Conv.rewr_conv rule
    1.34 +      end
    1.35      val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
    1.36 -    val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs)
    1.37 -    val lconv = move_to_front lpath
    1.38 -    val rconv = move_to_front rpath
    1.39 -    val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    1.40 -    val conv = conv1 then_conv Conv.rewr_conv rule
    1.41 +    val common = find_all_common coeff_ord (atoms lhs) (atoms rhs)
    1.42 +    val conv =
    1.43 +      if null common then Conv.no_conv
    1.44 +      else Conv.every_conv (map cancel1_conv common)
    1.45    in conv ct end
    1.46 -    handle Cancel => raise CTERM ("no_conversion", [])
    1.47  
    1.48  val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left})
    1.49  val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})