TFL/rules.ML
changeset 15798 016f3be5a5ec
parent 15574 b1d1b5bfc464
child 16853 33b886cbdc8f
--- a/TFL/rules.ML	Thu Apr 21 19:12:03 2005 +0200
+++ b/TFL/rules.ML	Thu Apr 21 19:13:03 2005 +0200
@@ -276,12 +276,12 @@
 local (* this is fragile *)
       val {prop,sign,...} = rep_thm spec
       val x = hd (tl (term_vars prop))
-      val (TVar (indx,_)) = type_of x
+      val cTV = ctyp_of sign (type_of x)
       val gspec = forall_intr (cterm_of sign x) spec
 in
 fun SPEC tm thm =
    let val {sign,T,...} = rep_cterm tm
-       val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
+       val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec
    in
       thm RS (forall_elim tm gspec')
    end
@@ -295,13 +295,14 @@
 (* Not optimized! Too complicated. *)
 local val {prop,sign,...} = rep_thm allI
       val [P] = add_term_vars (prop, [])
-      fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
-      fun ctm_theta s = map (fn (i,tm2) =>
+      fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
+      fun ctm_theta s = map (fn (i, (_, tm2)) =>
                              let val ctm2 = cterm_of s tm2
                              in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
                              end)
-      fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta,
-                                           ctm_theta s tm_theta)
+      fun certify s (ty_theta,tm_theta) =
+        (cty_theta s (Vartab.dest ty_theta),
+         ctm_theta s (Vartab.dest tm_theta))
 in
 fun GEN v th =
    let val gth = forall_intr v th