# HG changeset patch
# User berghofe
# Date 952696985 -3600
# Node ID d30df828a974d9918d97f4ada8fdee998978ce8f
# Parent  5902c02fa1227a081116016c00e1a5c018a99286
Type.typ_match now uses Vartab instead of association lists.

diff -r 5902c02fa122 -r d30df828a974 src/HOLCF/adm.ML
--- a/src/HOLCF/adm.ML	Fri Mar 10 15:02:04 2000 +0100
+++ b/src/HOLCF/adm.ML	Fri Mar 10 15:03:05 2000 +0100
@@ -109,8 +109,7 @@
   handle _ => l;
 
 
-(*** instantiation of adm_subst theorem (a bit tricky)
-     NOTE: maybe unnecessary (if "cont_thm RS adm_subst" works properly) ***)
+(*** instantiation of adm_subst theorem (a bit tricky) ***)
 
 fun inst_adm_subst_thm state i params s T subt t paths =
   let val {sign, maxidx, ...} = rep_thm state;
@@ -126,8 +125,8 @@
       val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
       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 ([], (tT, #T (rep_cterm tt)));
-      val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
+      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));
@@ -140,13 +139,7 @@
 fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
 
 
-(*** the admissibility tactic
-     NOTE:
-       (compose_tac (false, rule, 2) i) THEN
-       (rtac cont_thm i) THEN ...
-     could probably be replaced by
-       (rtac (cont_thm RS adm_subst) 1) THEN ...
-***)
+(*** the admissibility tactic ***)
 
 fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
       if name = adm_name then Some abs else None