1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 08 15:39:55 2011 +0200
1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 08 15:56:57 2011 +0200
1.3 @@ -5,8 +5,13 @@
1.4 a tactic to analyse instances of the fresh_fun.
1.5 *)
1.6
1.7 -(* First some functions that should be in the library *)
1.8 +(* First some functions that should be in the library *) (* FIXME really?? *)
1.9
1.10 +(* FIXME proper ML structure *)
1.11 +
1.12 +(* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
1.13 +
1.14 +(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
1.15 fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
1.16 let
1.17 val thy = theory_of_thm st;
1.18 @@ -25,7 +30,8 @@
1.19 (Thm.lift_rule cgoal th)
1.20 in
1.21 compose_tac (elim, th', nprems_of th) i st
1.22 - end handle Subscript => Seq.empty;
1.23 + end handle General.Subscript => Seq.empty;
1.24 +(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
1.25
1.26 val res_inst_tac_term =
1.27 gen_res_inst_tac_term (curry Thm.instantiate);
2.1 --- a/src/HOL/Nominal/nominal_permeq.ML Wed Jun 08 15:39:55 2011 +0200
2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Jun 08 15:56:57 2011 +0200
2.3 @@ -287,6 +287,7 @@
2.4 | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
2.5 | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
2.6
2.7 +(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
2.8 fun finite_guess_tac_i tactical ss i st =
2.9 let val goal = nth (cprems_of st) (i - 1)
2.10 in
2.11 @@ -318,12 +319,14 @@
2.12 end
2.13 | _ => Seq.empty
2.14 end
2.15 - handle Subscript => Seq.empty
2.16 + handle General.Subscript => Seq.empty
2.17 +(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
2.18
2.19
2.20 (* tactic that guesses whether an atom is fresh for an expression *)
2.21 (* it first collects all free variables and tries to show that the *)
2.22 (* support of these free variables (op supports) the goal *)
2.23 +(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
2.24 fun fresh_guess_tac_i tactical ss i st =
2.25 let
2.26 val goal = nth (cprems_of st) (i - 1)
2.27 @@ -361,7 +364,8 @@
2.28 | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",
2.29 (asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st
2.30 end
2.31 - handle Subscript => Seq.empty;
2.32 + handle General.Subscript => Seq.empty;
2.33 +(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
2.34
2.35 val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG_tac;
2.36
3.1 --- a/src/HOL/Statespace/state_space.ML Wed Jun 08 15:39:55 2011 +0200
3.2 +++ b/src/HOL/Statespace/state_space.ML Wed Jun 08 15:56:57 2011 +0200
3.3 @@ -360,7 +360,7 @@
3.4 val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
3.5 in all_comps end;
3.6
3.7 -fun take_upto i xs = List.take(xs,i) handle Subscript => xs;
3.8 +fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
3.9
3.10 fun statespace_definition state_type args name parents parent_comps components thy =
3.11 let
4.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 15:39:55 2011 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 15:56:57 2011 +0200
4.3 @@ -239,7 +239,7 @@
4.4 (* translation of #" " to #"/" *)
4.5 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
4.6 else
4.7 - let val digits = List.take (c::cs, 3) handle Subscript => [] in
4.8 + let val digits = List.take (c::cs, 3) handle General.Subscript => [] in
4.9 case Int.fromString (String.implode digits) of
4.10 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
4.11 | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
5.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 15:39:55 2011 +0200
5.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 15:56:57 2011 +0200
5.3 @@ -376,7 +376,7 @@
5.4 val p' = if adjustment > p then p else p - adjustment
5.5 val tm_p =
5.6 nth args p'
5.7 - handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
5.8 + handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
5.9 val _ = trace_msg ctxt (fn () =>
5.10 "path_finder: " ^ string_of_int p ^ " " ^
5.11 Syntax.string_of_term ctxt tm_p)
6.1 --- a/src/HOL/Tools/inductive_set.ML Wed Jun 08 15:39:55 2011 +0200
6.2 +++ b/src/HOL/Tools/inductive_set.ML Wed Jun 08 15:56:57 2011 +0200
6.3 @@ -206,7 +206,7 @@
6.4 | (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
6.5 SOME (SOME (_, (arity, _))) =>
6.6 (fold (infer_arities thy arities) (arity ~~ List.take (ts, length arity)) fs
6.7 - handle Subscript => error "infer_arities: bad term")
6.8 + handle General.Subscript => error "infer_arities: bad term")
6.9 | _ => fold (infer_arities thy arities) (map (pair NONE) ts)
6.10 (case optf of
6.11 NONE => fs
7.1 --- a/src/HOL/Tools/recdef.ML Wed Jun 08 15:39:55 2011 +0200
7.2 +++ b/src/HOL/Tools/recdef.ML Wed Jun 08 15:56:57 2011 +0200
7.3 @@ -261,7 +261,7 @@
7.4 NONE => error ("No recdef definition of constant: " ^ quote name)
7.5 | SOME {tcs, ...} => tcs);
7.6 val i = the_default 1 opt_i;
7.7 - val tc = nth tcs (i - 1) handle Subscript =>
7.8 + val tc = nth tcs (i - 1) handle General.Subscript =>
7.9 error ("No termination condition #" ^ string_of_int i ^
7.10 " in recdef definition of " ^ quote name);
7.11 in
8.1 --- a/src/Provers/order.ML Wed Jun 08 15:39:55 2011 +0200
8.2 +++ b/src/Provers/order.ML Wed Jun 08 15:56:57 2011 +0200
8.3 @@ -1247,9 +1247,9 @@
8.4 end
8.5 handle Contr p =>
8.6 (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
8.7 - handle Subscript => Seq.empty)
8.8 + handle General.Subscript => Seq.empty)
8.9 | Cannot => Seq.empty
8.10 - | Subscript => Seq.empty)
8.11 + | General.Subscript => Seq.empty)
8.12 end;
8.13
8.14 (* partial_tac - solves partial orders *)
9.1 --- a/src/Provers/quasi.ML Wed Jun 08 15:39:55 2011 +0200
9.2 +++ b/src/Provers/quasi.ML Wed Jun 08 15:56:57 2011 +0200
9.3 @@ -589,8 +589,8 @@
9.4 end
9.5 handle Contr p =>
9.6 (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
9.7 - handle Subscript => Seq.empty)
9.8 + handle General.Subscript => Seq.empty)
9.9 | Cannot => Seq.empty
9.10 - | Subscript => Seq.empty);
9.11 + | General.Subscript => Seq.empty);
9.12
9.13 end;
10.1 --- a/src/Provers/trancl.ML Wed Jun 08 15:39:55 2011 +0200
10.2 +++ b/src/Provers/trancl.ML Wed Jun 08 15:56:57 2011 +0200
10.3 @@ -567,6 +567,6 @@
10.4 val thms = map (prove thy rel' prems) prfs
10.5 in rtac (prove thy rel' thms prf) 1 end) ctxt n st
10.6 end
10.7 - handle Cannot => Seq.empty | Subscript => Seq.empty);
10.8 + handle Cannot => Seq.empty | General.Subscript => Seq.empty);
10.9
10.10 end;
11.1 --- a/src/Pure/Proof/reconstruct.ML Wed Jun 08 15:39:55 2011 +0200
11.2 +++ b/src/Pure/Proof/reconstruct.ML Wed Jun 08 15:56:57 2011 +0200
11.3 @@ -88,7 +88,7 @@
11.4 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
11.5 end
11.6 | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
11.7 - handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
11.8 + handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
11.9
11.10 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
11.11 Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
11.12 @@ -145,7 +145,7 @@
11.13 (Envir.head_norm env prop, prf, cnstrts, env, vTs);
11.14
11.15 fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs)
11.16 - handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
11.17 + handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
11.18 | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
11.19 let
11.20 val (T, env') =
12.1 --- a/src/Pure/envir.ML Wed Jun 08 15:39:55 2011 +0200
12.2 +++ b/src/Pure/envir.ML Wed Jun 08 15:56:57 2011 +0200
12.3 @@ -289,7 +289,7 @@
12.4 | fast Ts (Const (_, T)) = T
12.5 | fast Ts (Free (_, T)) = T
12.6 | fast Ts (Bound i) =
12.7 - (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
12.8 + (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
12.9 | fast Ts (Var (_, T)) = T
12.10 | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
12.11 in fast end;
13.1 --- a/src/Pure/library.ML Wed Jun 08 15:39:55 2011 +0200
13.2 +++ b/src/Pure/library.ML Wed Jun 08 15:56:57 2011 +0200
13.3 @@ -429,7 +429,7 @@
13.4 raise Subscript if list too short*)
13.5 fun nth xs i = List.nth (xs, i);
13.6
13.7 -fun nth_list xss i = nth xss i handle Subscript => [];
13.8 +fun nth_list xss i = nth xss i handle General.Subscript => [];
13.9
13.10 fun nth_map 0 f (x :: xs) = f x :: xs
13.11 | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
14.1 --- a/src/Pure/proofterm.ML Wed Jun 08 15:39:55 2011 +0200
14.2 +++ b/src/Pure/proofterm.ML Wed Jun 08 15:56:57 2011 +0200
14.3 @@ -529,7 +529,7 @@
14.4 fun subst' lev (Bound i) =
14.5 (if i<lev then raise Same.SAME (*var is locally bound*)
14.6 else incr_boundvars lev (nth args (i-lev))
14.7 - handle Subscript => Bound (i-n)) (*loose: change it*)
14.8 + handle General.Subscript => Bound (i-n)) (*loose: change it*)
14.9 | subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body)
14.10 | subst' lev (f $ t) = (subst' lev f $ substh' lev t
14.11 handle Same.SAME => f $ subst' lev t)
14.12 @@ -554,7 +554,7 @@
14.13 fun subst (PBound i) Plev tlev =
14.14 (if i < Plev then raise Same.SAME (*var is locally bound*)
14.15 else incr_pboundvars Plev tlev (nth args (i-Plev))
14.16 - handle Subscript => PBound (i-n) (*loose: change it*))
14.17 + handle General.Subscript => PBound (i-n) (*loose: change it*))
14.18 | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
14.19 | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
14.20 | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
15.1 --- a/src/Pure/sign.ML Wed Jun 08 15:39:55 2011 +0200
15.2 +++ b/src/Pure/sign.ML Wed Jun 08 15:56:57 2011 +0200
15.3 @@ -269,7 +269,7 @@
15.4 fun typ_of (_, Const (_, T)) = T
15.5 | typ_of (_, Free (_, T)) = T
15.6 | typ_of (_, Var (_, T)) = T
15.7 - | typ_of (bs, Bound i) = snd (nth bs i handle Subscript =>
15.8 + | typ_of (bs, Bound i) = snd (nth bs i handle General.Subscript =>
15.9 raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
15.10 | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
15.11 | typ_of (bs, t $ u) =
16.1 --- a/src/Pure/tactical.ML Wed Jun 08 15:39:55 2011 +0200
16.2 +++ b/src/Pure/tactical.ML Wed Jun 08 15:56:57 2011 +0200
16.3 @@ -354,7 +354,7 @@
16.4 orelse
16.5 not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
16.6 in Seq.filter diff (tac i st) end
16.7 - handle Subscript => Seq.empty (*no subgoal i*);
16.8 + handle General.Subscript => Seq.empty (*no subgoal i*);
16.9
16.10 (*Returns all states where some subgoals have been solved. For
16.11 subgoal-based tactics this means subgoal i has been solved
17.1 --- a/src/Pure/term.ML Wed Jun 08 15:39:55 2011 +0200
17.2 +++ b/src/Pure/term.ML Wed Jun 08 15:56:57 2011 +0200
17.3 @@ -311,7 +311,7 @@
17.4 fun type_of1 (Ts, Const (_,T)) = T
17.5 | type_of1 (Ts, Free (_,T)) = T
17.6 | type_of1 (Ts, Bound i) = (nth Ts i
17.7 - handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
17.8 + handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
17.9 | type_of1 (Ts, Var (_,T)) = T
17.10 | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
17.11 | type_of1 (Ts, f$u) =
17.12 @@ -336,7 +336,7 @@
17.13 | fastype_of1 (_, Const (_,T)) = T
17.14 | fastype_of1 (_, Free (_,T)) = T
17.15 | fastype_of1 (Ts, Bound i) = (nth Ts i
17.16 - handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
17.17 + handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
17.18 | fastype_of1 (_, Var (_,T)) = T
17.19 | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
17.20
17.21 @@ -668,7 +668,7 @@
17.22 fun subst (t as Bound i, lev) =
17.23 (if i < lev then raise Same.SAME (*var is locally bound*)
17.24 else incr_boundvars lev (nth args (i - lev))
17.25 - handle Subscript => Bound (i - n)) (*loose: change it*)
17.26 + handle General.Subscript => Bound (i - n)) (*loose: change it*)
17.27 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
17.28 | subst (f $ t, lev) =
17.29 (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
18.1 --- a/src/Pure/thm.ML Wed Jun 08 15:39:55 2011 +0200
18.2 +++ b/src/Pure/thm.ML Wed Jun 08 15:56:57 2011 +0200
18.3 @@ -1423,7 +1423,7 @@
18.4 and concl = Logic.strip_imp_concl prop;
18.5 val moved_prems = List.drop (prems, j)
18.6 and fixed_prems = List.take (prems, j)
18.7 - handle Subscript => raise THM ("permute_prems: j", j, [rl]);
18.8 + handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
18.9 val n_j = length moved_prems;
18.10 val m = if k < 0 then n_j + k else k;
18.11 val prop' =
19.1 --- a/src/Pure/type_infer_context.ML Wed Jun 08 15:39:55 2011 +0200
19.2 +++ b/src/Pure/type_infer_context.ML Wed Jun 08 15:56:57 2011 +0200
19.3 @@ -220,7 +220,7 @@
19.4 | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
19.5 | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
19.6 | inf bs (Bound i) tye_idx =
19.7 - (snd (nth bs i handle Subscript => err_loose i), tye_idx)
19.8 + (snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
19.9 | inf bs (Abs (x, T, t)) tye_idx =
19.10 let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
19.11 in (T --> U, tye_idx') end
20.1 --- a/src/Tools/WWW_Find/http_util.ML Wed Jun 08 15:39:55 2011 +0200
20.2 +++ b/src/Tools/WWW_Find/http_util.ML Wed Jun 08 15:56:57 2011 +0200
20.3 @@ -60,7 +60,7 @@
20.4 then f (Substring.full " "::pre::done, Substring.triml 1 post)
20.5 else let
20.6 val (c, rest) = Substring.splitAt (post, 3)
20.7 - handle Subscript =>
20.8 + handle General.Subscript =>
20.9 (Substring.full "%25", Substring.triml 1 post);
20.10 in f (to_char c::pre::done, rest) end
20.11 end;
21.1 --- a/src/Tools/induct.ML Wed Jun 08 15:39:55 2011 +0200
21.2 +++ b/src/Tools/induct.ML Wed Jun 08 15:56:57 2011 +0200
21.3 @@ -590,7 +590,7 @@
21.4 Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
21.5 |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
21.6 end
21.7 - end handle Subscript => Seq.empty;
21.8 + end handle General.Subscript => Seq.empty;
21.9
21.10 end;
21.11
22.1 --- a/src/Tools/subtyping.ML Wed Jun 08 15:39:55 2011 +0200
22.2 +++ b/src/Tools/subtyping.ML Wed Jun 08 15:56:57 2011 +0200
22.3 @@ -246,7 +246,7 @@
22.4 | gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
22.5 | gen cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs)
22.6 | gen cs bs (Bound i) tye_idx =
22.7 - (snd (nth bs i handle Subscript => err_loose i), tye_idx, cs)
22.8 + (snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs)
22.9 | gen cs bs (Abs (x, T, t)) tye_idx =
22.10 let val (U, tye_idx', cs') = gen cs ((x, T) :: bs) t tye_idx
22.11 in (T --> U, tye_idx', cs') end
22.12 @@ -636,7 +636,7 @@
22.13 let val T' = T;
22.14 in (Var (xi, T'), T') end
22.15 | insert bs (Bound i) =
22.16 - let val T = nth bs i handle Subscript => err_loose i;
22.17 + let val T = nth bs i handle General.Subscript => err_loose i;
22.18 in (Bound i, T) end
22.19 | insert bs (Abs (x, T, t)) =
22.20 let
22.21 @@ -671,7 +671,7 @@
22.22 | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
22.23 | inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
22.24 | inf bs (t as (Bound i)) tye_idx =
22.25 - (t, snd (nth bs i handle Subscript => err_loose i), tye_idx)
22.26 + (t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
22.27 | inf bs (Abs (x, T, t)) tye_idx =
22.28 let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx
22.29 in (Abs (x, T, t'), T --> U, tye_idx') end