more robust exception pattern General.Subscript;
authorwenzelm
Wed Jun 08 15:56:57 2011 +0200 (2011-06-08 ago)
changeset 432781fbdcebb364b
parent 43277 1fd31f859fc7
child 43279 6af741899bf6
more robust exception pattern General.Subscript;
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recdef.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Provers/trancl.ML
src/Pure/Proof/reconstruct.ML
src/Pure/envir.ML
src/Pure/library.ML
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/tactical.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type_infer_context.ML
src/Tools/WWW_Find/http_util.ML
src/Tools/induct.ML
src/Tools/subtyping.ML
     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