Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
move exception handlers outside of let block
authorhuffman
Sat, 28 Jul 2012 07:26:37 +0200
changeset 48571 d68b74435605
parent 48570 0c32d6267b93
child 48572 af0f5560ac94
move exception handlers outside of let block
src/HOL/Tools/group_cancel.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/nat_arith.ML file | annotate | diff | comparison | revisions 
--- 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})
--- 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})
isabelle