1.1 --- a/src/Provers/eqsubst.ML Wed Dec 31 00:08:14 2008 +0100
1.2 +++ b/src/Provers/eqsubst.ML Wed Dec 31 15:30:10 2008 +0100
1.3 @@ -1,13 +1,12 @@
1.4 (* Title: Provers/eqsubst.ML
1.5 - ID: $Id$
1.6 - Author: Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
1.7 + Author: Lucas Dixon, University of Edinburgh
1.8
1.9 A proof method to perform a substiution using an equation.
1.10 *)
1.11
1.12 signature EQSUBST =
1.13 sig
1.14 - (* a type abriviation for match information *)
1.15 + (* a type abbreviation for match information *)
1.16 type match =
1.17 ((indexname * (sort * typ)) list (* type instantiations *)
1.18 * (indexname * (typ * term)) list) (* term instantiations *)
1.19 @@ -224,7 +223,7 @@
1.20 (* is it OK to ignore the type instantiation info?
1.21 or should I be using it? *)
1.22 val typs_unify =
1.23 - SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
1.24 + SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
1.25 handle Type.TUNIFY => NONE;
1.26 in
1.27 case typs_unify of