removed some add-ons from modules that are relevant for the inference kernel;
authorwenzelm
Fri Nov 21 18:14:39 2014 +0100 (2014-11-21)
changeset 5902630b8a5825a9c
parent 59025 d885cff91200
child 59027 f9bee88c5912
removed some add-ons from modules that are relevant for the inference kernel;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/more_pattern.ML
src/Pure/more_unify.ML
src/Pure/pattern.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/ROOT	Fri Nov 21 13:18:56 2014 +0100
     1.2 +++ b/src/Pure/ROOT	Fri Nov 21 18:14:39 2014 +0100
     1.3 @@ -230,7 +230,9 @@
     1.4      "item_net.ML"
     1.5      "library.ML"
     1.6      "logic.ML"
     1.7 +    "more_pattern.ML"
     1.8      "more_thm.ML"
     1.9 +    "more_unify.ML"
    1.10      "morphism.ML"
    1.11      "name.ML"
    1.12      "net.ML"
     2.1 --- a/src/Pure/ROOT.ML	Fri Nov 21 13:18:56 2014 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Fri Nov 21 18:14:39 2014 +0100
     2.3 @@ -183,6 +183,8 @@
     2.4  use "theory.ML";
     2.5  use "proofterm.ML";
     2.6  use "thm.ML";
     2.7 +use "more_pattern.ML";
     2.8 +use "more_unify.ML";
     2.9  use "more_thm.ML";
    2.10  use "facts.ML";
    2.11  use "global_theory.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/more_pattern.ML	Fri Nov 21 18:14:39 2014 +0100
     3.3 @@ -0,0 +1,135 @@
     3.4 +(*  Title:      Pure/more_pattern.ML
     3.5 +    Author:     Tobias Nipkow, TU Muenchen
     3.6 +    Author:     Stefan Berghofer, TU Muenchen
     3.7 +
     3.8 +Add-ons to Higher-Order Patterns, outside the inference kernel.
     3.9 +*)
    3.10 +
    3.11 +signature PATTERN =
    3.12 +sig
    3.13 +  include PATTERN
    3.14 +  val matches: theory -> term * term -> bool
    3.15 +  val matchess: theory -> term list * term list -> bool
    3.16 +  val equiv: theory -> term * term -> bool
    3.17 +  val matches_subterm: theory -> term * term -> bool
    3.18 +  val first_order: term -> bool
    3.19 +  val pattern: term -> bool
    3.20 +  val match_rew: theory -> term -> term * term -> (term * term) option
    3.21 +  val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
    3.22 +  val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
    3.23 +end;
    3.24 +
    3.25 +structure Pattern: PATTERN =
    3.26 +struct
    3.27 +
    3.28 +fun matches thy po =
    3.29 +  (Pattern.match thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;
    3.30 +
    3.31 +fun matchess thy (ps, os) =
    3.32 +  length ps = length os andalso
    3.33 +    ((fold (Pattern.match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true)
    3.34 +      handle Pattern.MATCH => false);
    3.35 +
    3.36 +fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
    3.37 +
    3.38 +
    3.39 +(* Does pat match a subterm of obj? *)
    3.40 +fun matches_subterm thy (pat, obj) =
    3.41 +  let
    3.42 +    fun msub bounds obj = matches thy (pat, obj) orelse
    3.43 +      (case obj of
    3.44 +        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
    3.45 +      | t $ u => msub bounds t orelse msub bounds u
    3.46 +      | _ => false)
    3.47 +  in msub 0 obj end;
    3.48 +
    3.49 +fun first_order (Abs (_, _, t)) = first_order t
    3.50 +  | first_order (t $ u) = first_order t andalso first_order u andalso not (is_Var t)
    3.51 +  | first_order _ = true;
    3.52 +
    3.53 +fun pattern (Abs (_, _, t)) = pattern t
    3.54 +  | pattern t =
    3.55 +      let val (head, args) = strip_comb t in
    3.56 +        if is_Var head then
    3.57 +          forall is_Bound args andalso not (has_duplicates (op aconv) args)
    3.58 +        else forall pattern args
    3.59 +      end;
    3.60 +
    3.61 +
    3.62 +(* rewriting -- simple but fast *)
    3.63 +
    3.64 +fun match_rew thy tm (tm1, tm2) =
    3.65 +  let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
    3.66 +    SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
    3.67 +      handle Pattern.MATCH => NONE
    3.68 +  end;
    3.69 +
    3.70 +fun gen_rewrite_term bot thy rules procs tm =
    3.71 +  let
    3.72 +    val skel0 = Bound 0;
    3.73 +
    3.74 +    fun variant_absfree bounds (x, T, t) =
    3.75 +      let
    3.76 +        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
    3.77 +        fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
    3.78 +      in (abs, t') end;
    3.79 +
    3.80 +    fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
    3.81 +      | rew tm =
    3.82 +          (case get_first (match_rew thy tm) rules of
    3.83 +            NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
    3.84 +          | x => x);
    3.85 +
    3.86 +    fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
    3.87 +            Abs (_, _, body) =>
    3.88 +              let val tm' = subst_bound (tm2, body)
    3.89 +              in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
    3.90 +          | _ =>
    3.91 +            let val (skel1, skel2) = (case skel of
    3.92 +                skel1 $ skel2 => (skel1, skel2)
    3.93 +              | _ => (skel0, skel0))
    3.94 +            in case r bounds skel1 tm1 of
    3.95 +                SOME tm1' => (case r bounds skel2 tm2 of
    3.96 +                    SOME tm2' => SOME (tm1' $ tm2')
    3.97 +                  | NONE => SOME (tm1' $ tm2))
    3.98 +              | NONE => (case r bounds skel2 tm2 of
    3.99 +                    SOME tm2' => SOME (tm1 $ tm2')
   3.100 +                  | NONE => NONE)
   3.101 +            end)
   3.102 +      | rew_sub r bounds skel (Abs body) =
   3.103 +          let
   3.104 +            val (abs, tm') = variant_absfree bounds body;
   3.105 +            val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
   3.106 +          in case r (bounds + 1) skel' tm' of
   3.107 +              SOME tm'' => SOME (abs tm'')
   3.108 +            | NONE => NONE
   3.109 +          end
   3.110 +      | rew_sub _ _ _ _ = NONE;
   3.111 +
   3.112 +    fun rew_bot bounds (Var _) _ = NONE
   3.113 +      | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
   3.114 +          SOME tm1 => (case rew tm1 of
   3.115 +              SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
   3.116 +            | NONE => SOME tm1)
   3.117 +        | NONE => (case rew tm of
   3.118 +              SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
   3.119 +            | NONE => NONE));
   3.120 +
   3.121 +    fun rew_top bounds _ tm = (case rew tm of
   3.122 +          SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
   3.123 +              SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
   3.124 +            | NONE => SOME tm1)
   3.125 +        | NONE => (case rew_sub rew_top bounds skel0 tm of
   3.126 +              SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
   3.127 +            | NONE => NONE));
   3.128 +
   3.129 +  in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
   3.130 +
   3.131 +val rewrite_term = gen_rewrite_term true;
   3.132 +val rewrite_term_top = gen_rewrite_term false;
   3.133 +
   3.134 +
   3.135 +open Pattern;
   3.136 +
   3.137 +end;
   3.138 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/more_unify.ML	Fri Nov 21 18:14:39 2014 +0100
     4.3 @@ -0,0 +1,85 @@
     4.4 +(*  Title:      Pure/more_unify.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Add-ons to Higher-Order Unification, outside the inference kernel.
     4.8 +*)
     4.9 +
    4.10 +signature UNIFY =
    4.11 +sig
    4.12 +  include UNIFY
    4.13 +  val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
    4.14 +  val matches_list: Context.generic -> term list -> term list -> bool
    4.15 +end;
    4.16 +
    4.17 +structure Unify: UNIFY =
    4.18 +struct
    4.19 +
    4.20 +(*Pattern matching*)
    4.21 +fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
    4.22 +  let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
    4.23 +  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
    4.24 +  handle Pattern.MATCH => Seq.empty;
    4.25 +
    4.26 +(*General matching -- keep variables disjoint*)
    4.27 +fun matchers _ [] = Seq.single (Envir.empty ~1)
    4.28 +  | matchers context pairs =
    4.29 +      let
    4.30 +        val thy = Context.theory_of context;
    4.31 +
    4.32 +        val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
    4.33 +        val offset = maxidx + 1;
    4.34 +        val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
    4.35 +        val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
    4.36 +
    4.37 +        val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
    4.38 +        val pat_vars = fold (Term.add_vars o #1) pairs' [];
    4.39 +
    4.40 +        val decr_indexesT =
    4.41 +          Term.map_atyps (fn T as TVar ((x, i), S) =>
    4.42 +            if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
    4.43 +        val decr_indexes =
    4.44 +          Term.map_types decr_indexesT #>
    4.45 +          Term.map_aterms (fn t as Var ((x, i), T) =>
    4.46 +            if i > maxidx then Var ((x, i - offset), T) else t | t => t);
    4.47 +
    4.48 +        fun norm_tvar env ((x, i), S) =
    4.49 +          let
    4.50 +            val tyenv = Envir.type_env env;
    4.51 +            val T' = Envir.norm_type tyenv (TVar ((x, i), S));
    4.52 +          in
    4.53 +            if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE
    4.54 +            else SOME ((x, i - offset), (S, decr_indexesT T'))
    4.55 +          end;
    4.56 +
    4.57 +        fun norm_var env ((x, i), T) =
    4.58 +          let
    4.59 +            val tyenv = Envir.type_env env;
    4.60 +            val T' = Envir.norm_type tyenv T;
    4.61 +            val t' = Envir.norm_term env (Var ((x, i), T'));
    4.62 +          in
    4.63 +            if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE
    4.64 +            else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t'))
    4.65 +          end;
    4.66 +
    4.67 +        fun result env =
    4.68 +          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
    4.69 +            SOME (Envir.Envir {maxidx = maxidx,
    4.70 +              tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars),
    4.71 +              tenv = Vartab.make (map_filter (norm_var env) pat_vars)})
    4.72 +          else NONE;
    4.73 +
    4.74 +        val empty = Envir.empty maxidx';
    4.75 +      in
    4.76 +        Seq.append
    4.77 +          (Seq.map_filter result (Unify.smash_unifiers context pairs' empty))
    4.78 +          (first_order_matchers thy pairs empty)
    4.79 +      end;
    4.80 +
    4.81 +fun matches_list context ps os =
    4.82 +  length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
    4.83 +
    4.84 +
    4.85 +open Unify;
    4.86 +
    4.87 +end;
    4.88 +
     5.1 --- a/src/Pure/pattern.ML	Fri Nov 21 13:18:56 2014 +0100
     5.2 +++ b/src/Pure/pattern.ML	Fri Nov 21 18:14:39 2014 +0100
     5.3 @@ -22,15 +22,6 @@
     5.4    val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
     5.5    val first_order_match: theory -> term * term
     5.6      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
     5.7 -  val matches: theory -> term * term -> bool
     5.8 -  val matchess: theory -> term list * term list -> bool
     5.9 -  val equiv: theory -> term * term -> bool
    5.10 -  val matches_subterm: theory -> term * term -> bool
    5.11 -  val first_order: term -> bool
    5.12 -  val pattern: term -> bool
    5.13 -  val match_rew: theory -> term -> term * term -> (term * term) option
    5.14 -  val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
    5.15 -  val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
    5.16  end;
    5.17  
    5.18  structure Pattern: PATTERN =
    5.19 @@ -383,110 +374,5 @@
    5.20    val envir' = apfst (typ_match thy (pT, oT)) envir;
    5.21  in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
    5.22  
    5.23 -fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    5.24 -
    5.25 -fun matchess thy (ps, os) =
    5.26 -  length ps = length os andalso
    5.27 -    ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);
    5.28 -
    5.29 -fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
    5.30 -
    5.31 -
    5.32 -(* Does pat match a subterm of obj? *)
    5.33 -fun matches_subterm thy (pat, obj) =
    5.34 -  let
    5.35 -    fun msub bounds obj = matches thy (pat, obj) orelse
    5.36 -      (case obj of
    5.37 -        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
    5.38 -      | t $ u => msub bounds t orelse msub bounds u
    5.39 -      | _ => false)
    5.40 -  in msub 0 obj end;
    5.41 -
    5.42 -fun first_order(Abs(_,_,t)) = first_order t
    5.43 -  | first_order(t $ u) = first_order t andalso first_order u andalso
    5.44 -                         not(is_Var t)
    5.45 -  | first_order _ = true;
    5.46 -
    5.47 -fun pattern (Abs (_, _, t)) = pattern t
    5.48 -  | pattern t =
    5.49 -      let val (head, args) = strip_comb t in
    5.50 -        if is_Var head then
    5.51 -          forall is_Bound args andalso not (has_duplicates (op aconv) args)
    5.52 -        else forall pattern args
    5.53 -      end;
    5.54 -
    5.55 -
    5.56 -(* rewriting -- simple but fast *)
    5.57 -
    5.58 -fun match_rew thy tm (tm1, tm2) =
    5.59 -  let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
    5.60 -    SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
    5.61 -      handle MATCH => NONE
    5.62 -  end;
    5.63 -
    5.64 -fun gen_rewrite_term bot thy rules procs tm =
    5.65 -  let
    5.66 -    val skel0 = Bound 0;
    5.67 -
    5.68 -    fun variant_absfree bounds (x, T, t) =
    5.69 -      let
    5.70 -        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
    5.71 -        fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
    5.72 -      in (abs, t') end;
    5.73 -
    5.74 -    fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
    5.75 -      | rew tm =
    5.76 -          (case get_first (match_rew thy tm) rules of
    5.77 -            NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
    5.78 -          | x => x);
    5.79 -
    5.80 -    fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
    5.81 -            Abs (_, _, body) =>
    5.82 -              let val tm' = subst_bound (tm2, body)
    5.83 -              in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
    5.84 -          | _ =>
    5.85 -            let val (skel1, skel2) = (case skel of
    5.86 -                skel1 $ skel2 => (skel1, skel2)
    5.87 -              | _ => (skel0, skel0))
    5.88 -            in case r bounds skel1 tm1 of
    5.89 -                SOME tm1' => (case r bounds skel2 tm2 of
    5.90 -                    SOME tm2' => SOME (tm1' $ tm2')
    5.91 -                  | NONE => SOME (tm1' $ tm2))
    5.92 -              | NONE => (case r bounds skel2 tm2 of
    5.93 -                    SOME tm2' => SOME (tm1 $ tm2')
    5.94 -                  | NONE => NONE)
    5.95 -            end)
    5.96 -      | rew_sub r bounds skel (Abs body) =
    5.97 -          let
    5.98 -            val (abs, tm') = variant_absfree bounds body;
    5.99 -            val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
   5.100 -          in case r (bounds + 1) skel' tm' of
   5.101 -              SOME tm'' => SOME (abs tm'')
   5.102 -            | NONE => NONE
   5.103 -          end
   5.104 -      | rew_sub _ _ _ _ = NONE;
   5.105 -
   5.106 -    fun rew_bot bounds (Var _) _ = NONE
   5.107 -      | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
   5.108 -          SOME tm1 => (case rew tm1 of
   5.109 -              SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
   5.110 -            | NONE => SOME tm1)
   5.111 -        | NONE => (case rew tm of
   5.112 -              SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
   5.113 -            | NONE => NONE));
   5.114 -
   5.115 -    fun rew_top bounds _ tm = (case rew tm of
   5.116 -          SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
   5.117 -              SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
   5.118 -            | NONE => SOME tm1)
   5.119 -        | NONE => (case rew_sub rew_top bounds skel0 tm of
   5.120 -              SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
   5.121 -            | NONE => NONE));
   5.122 -
   5.123 -  in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
   5.124 -
   5.125 -val rewrite_term = gen_rewrite_term true;
   5.126 -val rewrite_term_top = gen_rewrite_term false;
   5.127 -
   5.128  end;
   5.129  
     6.1 --- a/src/Pure/unify.ML	Fri Nov 21 13:18:56 2014 +0100
     6.2 +++ b/src/Pure/unify.ML	Fri Nov 21 18:14:39 2014 +0100
     6.3 @@ -24,8 +24,6 @@
     6.4    val unifiers: Context.generic * Envir.env * ((term * term) list) ->
     6.5      (Envir.env * (term * term) list) Seq.seq
     6.6    val smash_unifiers: Context.generic -> (term * term) list -> Envir.env -> Envir.env Seq.seq
     6.7 -  val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
     6.8 -  val matches_list: Context.generic -> term list -> term list -> bool
     6.9  end
    6.10  
    6.11  structure Unify : UNIFY =
    6.12 @@ -664,69 +662,4 @@
    6.13  fun smash_unifiers context tus env =
    6.14    Seq.map smash_flexflex (unifiers (context, env, tus));
    6.15  
    6.16 -
    6.17 -(*Pattern matching*)
    6.18 -fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
    6.19 -  let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
    6.20 -  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
    6.21 -  handle Pattern.MATCH => Seq.empty;
    6.22 -
    6.23 -(*General matching -- keep variables disjoint*)
    6.24 -fun matchers _ [] = Seq.single (Envir.empty ~1)
    6.25 -  | matchers context pairs =
    6.26 -      let
    6.27 -        val thy = Context.theory_of context;
    6.28 -
    6.29 -        val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
    6.30 -        val offset = maxidx + 1;
    6.31 -        val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
    6.32 -        val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
    6.33 -
    6.34 -        val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
    6.35 -        val pat_vars = fold (Term.add_vars o #1) pairs' [];
    6.36 -
    6.37 -        val decr_indexesT =
    6.38 -          Term.map_atyps (fn T as TVar ((x, i), S) =>
    6.39 -            if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
    6.40 -        val decr_indexes =
    6.41 -          Term.map_types decr_indexesT #>
    6.42 -          Term.map_aterms (fn t as Var ((x, i), T) =>
    6.43 -            if i > maxidx then Var ((x, i - offset), T) else t | t => t);
    6.44 -
    6.45 -        fun norm_tvar env ((x, i), S) =
    6.46 -          let
    6.47 -            val tyenv = Envir.type_env env;
    6.48 -            val T' = Envir.norm_type tyenv (TVar ((x, i), S));
    6.49 -          in
    6.50 -            if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE
    6.51 -            else SOME ((x, i - offset), (S, decr_indexesT T'))
    6.52 -          end;
    6.53 -
    6.54 -        fun norm_var env ((x, i), T) =
    6.55 -          let
    6.56 -            val tyenv = Envir.type_env env;
    6.57 -            val T' = Envir.norm_type tyenv T;
    6.58 -            val t' = Envir.norm_term env (Var ((x, i), T'));
    6.59 -          in
    6.60 -            if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE
    6.61 -            else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t'))
    6.62 -          end;
    6.63 -
    6.64 -        fun result env =
    6.65 -          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
    6.66 -            SOME (Envir.Envir {maxidx = maxidx,
    6.67 -              tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars),
    6.68 -              tenv = Vartab.make (map_filter (norm_var env) pat_vars)})
    6.69 -          else NONE;
    6.70 -
    6.71 -        val empty = Envir.empty maxidx';
    6.72 -      in
    6.73 -        Seq.append
    6.74 -          (Seq.map_filter result (smash_unifiers context pairs' empty))
    6.75 -          (first_order_matchers thy pairs empty)
    6.76 -      end;
    6.77 -
    6.78 -fun matches_list context ps os =
    6.79 -  length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
    6.80 -
    6.81  end;