--- 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
--- 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
(
--- 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
--- 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';
--- 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)
--- 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
--- 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,
--- 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