src/HOL/Tools/nat_arith.ML

     val (lpath, rpath) = find_common Term_Ord.term_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
-  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})
 val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
 val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})