--- a/src/HOL/Tools/nat_arith.ML Fri Jul 27 23:14:55 2012 +0200
+++ b/src/HOL/Tools/nat_arith.ML Sat Jul 28 07:26:37 2012 +0200
@@ -62,7 +62,8 @@
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
- in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
+ in conv ct end
+ handle Cancel => raise CTERM ("no_conversion", [])
val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})