changeset 29270 | 0eade173f77e |
parent 29265 | 5b4247055bd7 |
child 31723 | f5cafe803b55 |
--- a/src/HOL/Tools/TFL/casesplit.ML Wed Dec 31 15:30:10 2008 +0100 +++ b/src/HOL/Tools/TFL/casesplit.ML Wed Dec 31 18:53:16 2008 +0100 @@ -123,7 +123,7 @@ val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm)); - val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm); + val casethm_tvars = OldTerm.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)))) =>