# HG changeset patch # User wenzelm # Date 1307541417 -7200 # Node ID 1fbdcebb364bbdaa92a03456a3467fba55735f6d # Parent 1fd31f859fc796444bd81c2bf78a312b8471d215 more robust exception pattern General.Subscript; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Nominal/nominal_fresh_fun.ML --- 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); diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Nominal/nominal_permeq.ML --- 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 _\_, 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; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Statespace/state_space.ML --- 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Tools/ATP/atp_translate.ML --- 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 *) diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Tools/Metis/metis_reconstruct.ML --- 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) diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Tools/inductive_set.ML --- 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Tools/recdef.ML --- 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Provers/order.ML --- 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 *) diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Provers/quasi.ML --- 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; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Provers/trancl.ML --- 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; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/Proof/reconstruct.ML --- 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') = diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/envir.ML --- 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; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/library.ML --- 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/proofterm.ML --- 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 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/sign.ML --- 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) = diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/tactical.ML --- 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/term.ML --- 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) diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/thm.ML --- 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' = diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Pure/type_infer_context.ML --- 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 diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Tools/WWW_Find/http_util.ML --- 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; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Tools/induct.ML --- 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; diff -r 1fd31f859fc7 -r 1fbdcebb364b src/Tools/subtyping.ML --- 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