# HG changeset patch # User wenzelm # Date 1222681607 -7200 # Node ID 389c5e494605d18f8496d40b6e6620b80d922031 # Parent 72695dd4395dd1d079166668e97df25036d47c84 handle _ should be avoided (spurious Interrupt will spoil the game); diff -r 72695dd4395d -r 389c5e494605 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon Sep 29 11:46:47 2008 +0200 @@ -1250,7 +1250,7 @@ then SOME (newstr,valOf(Int.fromString idx)) else NONE end - handle _ => NONE + handle _ => NONE (* FIXME avoid handle _ *) fun rewrite_hol4_term t thy = let @@ -1283,7 +1283,7 @@ handle ERROR _ => (case split_name thmname of SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1)) - handle _ => NONE) + handle _ => NONE) (* FIXME avoid handle _ *) | NONE => NONE)) in case th1 of @@ -1339,7 +1339,7 @@ end in case b of - NONE => (warn () handle _ => (); (a,b)) + NONE => (warn () handle _ => (); (a,b)) (* FIXME avoid handle _ *) | _ => (a, b) end diff -r 72695dd4395d -r 389c5e494605 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Import/shuffler.ML Mon Sep 29 11:46:47 2008 +0200 @@ -66,14 +66,14 @@ Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection | Const("==",_) $ _ $ _ => th | _ => raise THM("Not an equality",0,[th])) - handle _ => raise THM("Couldn't make meta equality",0,[th]) + handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *) fun mk_obj_eq th = (case concl_of th of Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq | _ => raise THM("Not an equality",0,[th])) - handle _ => raise THM("Couldn't make object equality",0,[th]) + handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *) structure ShuffleData = TheoryDataFun ( diff -r 72695dd4395d -r 389c5e494605 src/HOL/Matrix/cplex/matrixlp.ML --- a/src/HOL/Matrix/cplex/matrixlp.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Matrix/cplex/matrixlp.ML Mon Sep 29 11:46:47 2008 +0200 @@ -83,7 +83,7 @@ let val simp_th = matrix_compute (cprop_of th) val th = strip_shyps (equal_elim simp_th th) - fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th + fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *) in removeTrue th end diff -r 72695dd4395d -r 389c5e494605 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Sep 29 11:46:47 2008 +0200 @@ -86,7 +86,7 @@ (term_frees goal @ bvs); (* build the tuple *) val s = (Library.foldr1 (fn (v, s) => - HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ; + HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ; (* FIXME avoid handle _ *) val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename; val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; val exists_fresh' = at_name_inst_thm RS at_exists_fresh'; diff -r 72695dd4395d -r 389c5e494605 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Sep 29 11:46:47 2008 +0200 @@ -557,7 +557,7 @@ | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => - (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") + (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *) | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2) | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) diff -r 72695dd4395d -r 389c5e494605 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Tools/meson.ML Mon Sep 29 11:46:47 2008 +0200 @@ -88,7 +88,7 @@ val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0) val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) in thA RS (cterm_instantiate ct_pairs thB) end - handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); + handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *) fun flexflex_first_order th = case (tpairs_of th) of diff -r 72695dd4395d -r 389c5e494605 src/HOL/Tools/polyhash.ML --- a/src/HOL/Tools/polyhash.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/HOL/Tools/polyhash.ML Mon Sep 29 11:46:47 2008 +0200 @@ -157,7 +157,7 @@ end fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1)) in - (bucket 0) handle _ => (); + (bucket 0) handle _ => (); (* FIXME avoid handle _ *) table := newArr end else () @@ -362,7 +362,7 @@ Array.update (newArr, i, Array.sub(arr, i)); mapTbl (i+1)) in - (mapTbl 0) handle _ => (); + (mapTbl 0) handle _ => (); (* FIXME avoid handle _ *) HT{hashVal=hashVal, sameKey=sameKey, table = ref newArr, diff -r 72695dd4395d -r 389c5e494605 src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Mon Sep 29 10:58:04 2008 +0200 +++ b/src/Pure/ProofGeneral/pgip_types.ML Mon Sep 29 11:46:47 2008 +0200 @@ -211,7 +211,7 @@ (case XML.parse_string s of SOME s => s | NONE => raise PGIP ("Expected a non-empty string: " ^ quote s)) - handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s) + handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s) (* FIXME avoid handle _ *) val int_to_pgstring = signed_string_of_int