# HG changeset patch
# User huffman
# Date 1343453197 -7200
# Node ID d68b74435605248770dbbe0516e90dc2ff593692
# Parent  0c32d6267b935d5df4f0c532258bd1d3f75a517a
move exception handlers outside of let block

diff -r 0c32d6267b93 -r d68b74435605 src/HOL/Tools/group_cancel.ML
--- a/src/HOL/Tools/group_cancel.ML	Fri Jul 27 23:14:55 2012 +0200
+++ b/src/HOL/Tools/group_cancel.ML	Sat Jul 28 07:26:37 2012 +0200
@@ -72,7 +72,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 add_diff_cancel_left})
 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
diff -r 0c32d6267b93 -r d68b74435605 src/HOL/Tools/nat_arith.ML
--- 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})