handle _ should be avoided (spurious Interrupt will spoil the game);
authorwenzelm
Mon Sep 29 11:46:47 2008 +0200 (2008-09-29)
changeset 28397389c5e494605
parent 28396 72695dd4395d
child 28398 9aa3216e5f31
handle _ should be avoided (spurious Interrupt will spoil the game);
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/polyhash.ML
src/Pure/ProofGeneral/pgip_types.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Sep 29 10:58:04 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Sep 29 11:46:47 2008 +0200
     1.3 @@ -1250,7 +1250,7 @@
     1.4          then SOME (newstr,valOf(Int.fromString idx))
     1.5          else NONE
     1.6      end
     1.7 -    handle _ => NONE
     1.8 +    handle _ => NONE  (* FIXME avoid handle _ *)
     1.9  
    1.10  fun rewrite_hol4_term t thy =
    1.11      let
    1.12 @@ -1283,7 +1283,7 @@
    1.13                             handle ERROR _ =>
    1.14                                    (case split_name thmname of
    1.15                                         SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
    1.16 -                                                               handle _ => NONE)
    1.17 +                                                               handle _ => NONE)  (* FIXME avoid handle _ *)
    1.18                                       | NONE => NONE))
    1.19              in
    1.20                  case th1 of
    1.21 @@ -1339,7 +1339,7 @@
    1.22          end
    1.23    in
    1.24        case b of
    1.25 -          NONE => (warn () handle _ => (); (a,b))
    1.26 +          NONE => (warn () handle _ => (); (a,b)) (* FIXME avoid handle _ *)
    1.27          | _ => (a, b)
    1.28    end
    1.29  
     2.1 --- a/src/HOL/Import/shuffler.ML	Mon Sep 29 10:58:04 2008 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Mon Sep 29 11:46:47 2008 +0200
     2.3 @@ -66,14 +66,14 @@
     2.4           Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
     2.5         | Const("==",_) $ _ $ _ => th
     2.6         | _ => raise THM("Not an equality",0,[th]))
     2.7 -    handle _ => raise THM("Couldn't make meta equality",0,[th])
     2.8 +    handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
     2.9  
    2.10  fun mk_obj_eq th =
    2.11      (case concl_of th of
    2.12           Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
    2.13         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
    2.14         | _ => raise THM("Not an equality",0,[th]))
    2.15 -    handle _ => raise THM("Couldn't make object equality",0,[th])
    2.16 +    handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
    2.17  
    2.18  structure ShuffleData = TheoryDataFun
    2.19  (
     3.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Mon Sep 29 10:58:04 2008 +0200
     3.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Mon Sep 29 11:46:47 2008 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4      let
     3.5          val simp_th = matrix_compute (cprop_of th)
     3.6          val th = strip_shyps (equal_elim simp_th th)
     3.7 -        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
     3.8 +        fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
     3.9      in
    3.10          removeTrue th
    3.11      end
     4.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Sep 29 10:58:04 2008 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Sep 29 11:46:47 2008 +0200
     4.3 @@ -86,7 +86,7 @@
     4.4       (term_frees goal @ bvs);
     4.5  (* build the tuple *)
     4.6     val s = (Library.foldr1 (fn (v, s) =>
     4.7 -     HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;
     4.8 +     HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;  (* FIXME avoid handle _ *)
     4.9     val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename;
    4.10     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    4.11     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
     5.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 29 10:58:04 2008 +0200
     5.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 29 11:46:47 2008 +0200
     5.3 @@ -557,7 +557,7 @@
     5.4    | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
     5.5    | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
     5.6    | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => 
     5.7 -      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
     5.8 +      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
     5.9    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    5.10    | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    5.11    | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
     6.1 --- a/src/HOL/Tools/meson.ML	Mon Sep 29 10:58:04 2008 +0200
     6.2 +++ b/src/HOL/Tools/meson.ML	Mon Sep 29 11:46:47 2008 +0200
     6.3 @@ -88,7 +88,7 @@
     6.4        val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
     6.5        val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
     6.6    in  thA RS (cterm_instantiate ct_pairs thB)  end
     6.7 -  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
     6.8 +  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);  (* FIXME avoid handle _ *)
     6.9  
    6.10  fun flexflex_first_order th =
    6.11    case (tpairs_of th) of
     7.1 --- a/src/HOL/Tools/polyhash.ML	Mon Sep 29 10:58:04 2008 +0200
     7.2 +++ b/src/HOL/Tools/polyhash.ML	Mon Sep 29 11:46:47 2008 +0200
     7.3 @@ -157,7 +157,7 @@
     7.4  			end
     7.5  		  fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1))
     7.6  		  in
     7.7 -		    (bucket 0) handle _ => ();
     7.8 +		    (bucket 0) handle _ => ();  (* FIXME avoid handle _ *)
     7.9  		    table := newArr
    7.10  		  end
    7.11  		else ()
    7.12 @@ -362,7 +362,7 @@
    7.13  		Array.update (newArr, i, Array.sub(arr, i));
    7.14  		mapTbl (i+1))
    7.15  	  in
    7.16 -	    (mapTbl 0) handle _ => ();
    7.17 +	    (mapTbl 0) handle _ => ();  (* FIXME avoid handle _ *)
    7.18  	    HT{hashVal=hashVal, 
    7.19  	       sameKey=sameKey,
    7.20  	       table = ref newArr, 
     8.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Mon Sep 29 10:58:04 2008 +0200
     8.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Mon Sep 29 11:46:47 2008 +0200
     8.3 @@ -211,7 +211,7 @@
     8.4      (case XML.parse_string s of
     8.5           SOME s => s
     8.6         | NONE => raise PGIP ("Expected a non-empty string: " ^ quote s))
     8.7 -    handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)
     8.8 +    handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)  (* FIXME avoid handle _ *)
     8.9  
    8.10  val int_to_pgstring = signed_string_of_int
    8.11