--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 08 15:56:57 2011 +0200
@@ -5,8 +5,13 @@
a tactic to analyse instances of the fresh_fun.
*)
-(* First some functions that should be in the library *)
+(* First some functions that should be in the library *) (* FIXME really?? *)
+
+(* FIXME proper ML structure *)
+(* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
+
+(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
let
val thy = theory_of_thm st;
@@ -25,7 +30,8 @@
(Thm.lift_rule cgoal th)
in
compose_tac (elim, th', nprems_of th) i st
- end handle Subscript => Seq.empty;
+ end handle General.Subscript => Seq.empty;
+(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
val res_inst_tac_term =
gen_res_inst_tac_term (curry Thm.instantiate);
--- a/src/HOL/Nominal/nominal_permeq.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Jun 08 15:56:57 2011 +0200
@@ -287,6 +287,7 @@
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
+(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun finite_guess_tac_i tactical ss i st =
let val goal = nth (cprems_of st) (i - 1)
in
@@ -318,12 +319,14 @@
end
| _ => Seq.empty
end
- handle Subscript => Seq.empty
+ handle General.Subscript => Seq.empty
+(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
(* tactic that guesses whether an atom is fresh for an expression *)
(* it first collects all free variables and tries to show that the *)
(* support of these free variables (op supports) the goal *)
+(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun fresh_guess_tac_i tactical ss i st =
let
val goal = nth (cprems_of st) (i - 1)
@@ -361,7 +364,8 @@
| _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",
(asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st
end
- handle Subscript => Seq.empty;
+ handle General.Subscript => Seq.empty;
+(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG_tac;
--- a/src/HOL/Statespace/state_space.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Jun 08 15:56:57 2011 +0200
@@ -360,7 +360,7 @@
val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
in all_comps end;
-fun take_upto i xs = List.take(xs,i) handle Subscript => xs;
+fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
fun statespace_definition state_type args name parents parent_comps components thy =
let
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 15:56:57 2011 +0200
@@ -239,7 +239,7 @@
(* translation of #" " to #"/" *)
un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
else
- let val digits = List.take (c::cs, 3) handle Subscript => [] in
+ let val digits = List.take (c::cs, 3) handle General.Subscript => [] in
case Int.fromString (String.implode digits) of
SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
| NONE => un (c:: #"_"::rcs) cs (* ERROR *)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 15:56:57 2011 +0200
@@ -376,7 +376,7 @@
val p' = if adjustment > p then p else p - adjustment
val tm_p =
nth args p'
- handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
+ handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
val _ = trace_msg ctxt (fn () =>
"path_finder: " ^ string_of_int p ^ " " ^
Syntax.string_of_term ctxt tm_p)
--- a/src/HOL/Tools/inductive_set.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Jun 08 15:56:57 2011 +0200
@@ -206,7 +206,7 @@
| (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
SOME (SOME (_, (arity, _))) =>
(fold (infer_arities thy arities) (arity ~~ List.take (ts, length arity)) fs
- handle Subscript => error "infer_arities: bad term")
+ handle General.Subscript => error "infer_arities: bad term")
| _ => fold (infer_arities thy arities) (map (pair NONE) ts)
(case optf of
NONE => fs
--- a/src/HOL/Tools/recdef.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Tools/recdef.ML Wed Jun 08 15:56:57 2011 +0200
@@ -261,7 +261,7 @@
NONE => error ("No recdef definition of constant: " ^ quote name)
| SOME {tcs, ...} => tcs);
val i = the_default 1 opt_i;
- val tc = nth tcs (i - 1) handle Subscript =>
+ val tc = nth tcs (i - 1) handle General.Subscript =>
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
--- a/src/Provers/order.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Provers/order.ML Wed Jun 08 15:56:57 2011 +0200
@@ -1247,9 +1247,9 @@
end
handle Contr p =>
(Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
- handle Subscript => Seq.empty)
+ handle General.Subscript => Seq.empty)
| Cannot => Seq.empty
- | Subscript => Seq.empty)
+ | General.Subscript => Seq.empty)
end;
(* partial_tac - solves partial orders *)
--- a/src/Provers/quasi.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Provers/quasi.ML Wed Jun 08 15:56:57 2011 +0200
@@ -589,8 +589,8 @@
end
handle Contr p =>
(Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
- handle Subscript => Seq.empty)
+ handle General.Subscript => Seq.empty)
| Cannot => Seq.empty
- | Subscript => Seq.empty);
+ | General.Subscript => Seq.empty);
end;
--- a/src/Provers/trancl.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Provers/trancl.ML Wed Jun 08 15:56:57 2011 +0200
@@ -567,6 +567,6 @@
val thms = map (prove thy rel' prems) prfs
in rtac (prove thy rel' thms prf) 1 end) ctxt n st
end
- handle Cannot => Seq.empty | Subscript => Seq.empty);
+ handle Cannot => Seq.empty | General.Subscript => Seq.empty);
end;
--- a/src/Pure/Proof/reconstruct.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML Wed Jun 08 15:56:57 2011 +0200
@@ -88,7 +88,7 @@
in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
end
| infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
- handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
+ handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
@@ -145,7 +145,7 @@
(Envir.head_norm env prop, prf, cnstrts, env, vTs);
fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs)
- handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
+ handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
| mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
let
val (T, env') =
--- a/src/Pure/envir.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/envir.ML Wed Jun 08 15:56:57 2011 +0200
@@ -289,7 +289,7 @@
| fast Ts (Const (_, T)) = T
| fast Ts (Free (_, T)) = T
| fast Ts (Bound i) =
- (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
+ (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
| fast Ts (Var (_, T)) = T
| fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
in fast end;
--- a/src/Pure/library.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/library.ML Wed Jun 08 15:56:57 2011 +0200
@@ -429,7 +429,7 @@
raise Subscript if list too short*)
fun nth xs i = List.nth (xs, i);
-fun nth_list xss i = nth xss i handle Subscript => [];
+fun nth_list xss i = nth xss i handle General.Subscript => [];
fun nth_map 0 f (x :: xs) = f x :: xs
| nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
--- a/src/Pure/proofterm.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/proofterm.ML Wed Jun 08 15:56:57 2011 +0200
@@ -529,7 +529,7 @@
fun subst' lev (Bound i) =
(if i<lev then raise Same.SAME (*var is locally bound*)
else incr_boundvars lev (nth args (i-lev))
- handle Subscript => Bound (i-n)) (*loose: change it*)
+ handle General.Subscript => Bound (i-n)) (*loose: change it*)
| subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body)
| subst' lev (f $ t) = (subst' lev f $ substh' lev t
handle Same.SAME => f $ subst' lev t)
@@ -554,7 +554,7 @@
fun subst (PBound i) Plev tlev =
(if i < Plev then raise Same.SAME (*var is locally bound*)
else incr_pboundvars Plev tlev (nth args (i-Plev))
- handle Subscript => PBound (i-n) (*loose: change it*))
+ handle General.Subscript => PBound (i-n) (*loose: change it*))
| subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
| subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
| subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
--- a/src/Pure/sign.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/sign.ML Wed Jun 08 15:56:57 2011 +0200
@@ -269,7 +269,7 @@
fun typ_of (_, Const (_, T)) = T
| typ_of (_, Free (_, T)) = T
| typ_of (_, Var (_, T)) = T
- | typ_of (bs, Bound i) = snd (nth bs i handle Subscript =>
+ | typ_of (bs, Bound i) = snd (nth bs i handle General.Subscript =>
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
| typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
| typ_of (bs, t $ u) =
--- a/src/Pure/tactical.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/tactical.ML Wed Jun 08 15:56:57 2011 +0200
@@ -354,7 +354,7 @@
orelse
not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
in Seq.filter diff (tac i st) end
- handle Subscript => Seq.empty (*no subgoal i*);
+ handle General.Subscript => Seq.empty (*no subgoal i*);
(*Returns all states where some subgoals have been solved. For
subgoal-based tactics this means subgoal i has been solved
--- a/src/Pure/term.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/term.ML Wed Jun 08 15:56:57 2011 +0200
@@ -311,7 +311,7 @@
fun type_of1 (Ts, Const (_,T)) = T
| type_of1 (Ts, Free (_,T)) = T
| type_of1 (Ts, Bound i) = (nth Ts i
- handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
+ handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
| type_of1 (Ts, Var (_,T)) = T
| type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
| type_of1 (Ts, f$u) =
@@ -336,7 +336,7 @@
| fastype_of1 (_, Const (_,T)) = T
| fastype_of1 (_, Free (_,T)) = T
| fastype_of1 (Ts, Bound i) = (nth Ts i
- handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
+ handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
| fastype_of1 (_, Var (_,T)) = T
| fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
@@ -668,7 +668,7 @@
fun subst (t as Bound i, lev) =
(if i < lev then raise Same.SAME (*var is locally bound*)
else incr_boundvars lev (nth args (i - lev))
- handle Subscript => Bound (i - n)) (*loose: change it*)
+ handle General.Subscript => Bound (i - n)) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
(subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
--- a/src/Pure/thm.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/thm.ML Wed Jun 08 15:56:57 2011 +0200
@@ -1423,7 +1423,7 @@
and concl = Logic.strip_imp_concl prop;
val moved_prems = List.drop (prems, j)
and fixed_prems = List.take (prems, j)
- handle Subscript => raise THM ("permute_prems: j", j, [rl]);
+ handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
val n_j = length moved_prems;
val m = if k < 0 then n_j + k else k;
val prop' =
--- a/src/Pure/type_infer_context.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/type_infer_context.ML Wed Jun 08 15:56:57 2011 +0200
@@ -220,7 +220,7 @@
| inf _ (Free (_, T)) tye_idx = (T, tye_idx)
| inf _ (Var (_, T)) tye_idx = (T, tye_idx)
| inf bs (Bound i) tye_idx =
- (snd (nth bs i handle Subscript => err_loose i), tye_idx)
+ (snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
| inf bs (Abs (x, T, t)) tye_idx =
let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
in (T --> U, tye_idx') end
--- a/src/Tools/WWW_Find/http_util.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Tools/WWW_Find/http_util.ML Wed Jun 08 15:56:57 2011 +0200
@@ -60,7 +60,7 @@
then f (Substring.full " "::pre::done, Substring.triml 1 post)
else let
val (c, rest) = Substring.splitAt (post, 3)
- handle Subscript =>
+ handle General.Subscript =>
(Substring.full "%25", Substring.triml 1 post);
in f (to_char c::pre::done, rest) end
end;
--- a/src/Tools/induct.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Tools/induct.ML Wed Jun 08 15:56:57 2011 +0200
@@ -590,7 +590,7 @@
Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
|> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
end
- end handle Subscript => Seq.empty;
+ end handle General.Subscript => Seq.empty;
end;
--- a/src/Tools/subtyping.ML Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Tools/subtyping.ML Wed Jun 08 15:56:57 2011 +0200
@@ -246,7 +246,7 @@
| gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
| gen cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs)
| gen cs bs (Bound i) tye_idx =
- (snd (nth bs i handle Subscript => err_loose i), tye_idx, cs)
+ (snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs)
| gen cs bs (Abs (x, T, t)) tye_idx =
let val (U, tye_idx', cs') = gen cs ((x, T) :: bs) t tye_idx
in (T --> U, tye_idx', cs') end
@@ -636,7 +636,7 @@
let val T' = T;
in (Var (xi, T'), T') end
| insert bs (Bound i) =
- let val T = nth bs i handle Subscript => err_loose i;
+ let val T = nth bs i handle General.Subscript => err_loose i;
in (Bound i, T) end
| insert bs (Abs (x, T, t)) =
let
@@ -671,7 +671,7 @@
| inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
| inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
| inf bs (t as (Bound i)) tye_idx =
- (t, snd (nth bs i handle Subscript => err_loose i), tye_idx)
+ (t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
| inf bs (Abs (x, T, t)) tye_idx =
let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx
in (Abs (x, T, t'), T --> U, tye_idx') end