move exception handlers outside of let block
authorhuffman
Sat Jul 28 07:26:37 2012 +0200 (2012-07-28)
changeset 48571d68b74435605
parent 48570 0c32d6267b93
child 48572 af0f5560ac94
move exception handlers outside of let block
src/HOL/Tools/group_cancel.ML
src/HOL/Tools/nat_arith.ML
     1.1 --- a/src/HOL/Tools/group_cancel.ML	Fri Jul 27 23:14:55 2012 +0200
     1.2 +++ b/src/HOL/Tools/group_cancel.ML	Sat Jul 28 07:26:37 2012 +0200
     1.3 @@ -72,7 +72,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 add_diff_cancel_left})
    1.12  val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
     2.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 23:14:55 2012 +0200
     2.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Jul 28 07:26:37 2012 +0200
     2.3 @@ -62,7 +62,8 @@
     2.4      val rconv = move_to_front rpath
     2.5      val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
     2.6      val conv = conv1 then_conv Conv.rewr_conv rule
     2.7 -  in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
     2.8 +  in conv ct end
     2.9 +    handle Cancel => raise CTERM ("no_conversion", [])
    2.10  
    2.11  val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
    2.12  val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})