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