TFL/casesplit.ML
changeset 16935 4d7f19d340e8
parent 16425 2427be27cc60
child 16978 e35b518bffc9
--- a/TFL/casesplit.ML	Thu Jul 28 15:19:49 2005 +0200
+++ b/TFL/casesplit.ML	Thu Jul 28 15:19:51 2005 +0200
@@ -156,13 +156,12 @@
 
       val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
        
-      val tsig = Sign.tsig_of sgn;
       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
       val (Pv, Dv, type_insts) = 
           case (Thm.concl_of case_thm) of 
             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => 
             (Pv, Dv, 
-             Type.typ_match tsig (Vartab.empty, (Dty, ty)))
+             Sign.typ_match sgn (Dty, ty) Vartab.empty)
           | _ => raise ERROR_MESSAGE ("not a valid case thm");
       val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
         (Vartab.dest type_insts);