src/HOLCF/adm.ML

--- a/src/HOLCF/adm.ML	Thu Apr 21 18:56:03 2005 +0200
+++ b/src/HOLCF/adm.ML	Thu Apr 21 18:57:18 2005 +0200
@@ -125,10 +125,11 @@
       val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
                      (make_term t [] paths 0));
       val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
-      val tye' = Vartab.dest (Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))));
-      val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye';
-      val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT));
-      val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT));
+      val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
+      val ctye = map (fn (ixn, (S, T)) =>
+        (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
+      val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
+      val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
       val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
   in rule' end;