src/HOL/Tools/nat_arith.ML
changeset 48571 d68b74435605
parent 48561 12aa0cb2b447
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 23:14:55 2012 +0200
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Jul 28 07:26:37 2012 +0200
     1.3 @@ -62,7 +62,8 @@
     1.4      val rconv = move_to_front rpath
     1.5      val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
     1.6      val conv = conv1 then_conv Conv.rewr_conv rule
     1.7 -  in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
     1.8 +  in conv ct end
     1.9 +    handle Cancel => raise CTERM ("no_conversion", [])
    1.10  
    1.11  val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
    1.12  val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})