--- a/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 20:53:43 2011 +0200
@@ -56,9 +56,9 @@
val abs_ct = ctermify abst;
val free_ct = ctermify x;
- val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
+ val casethm_vars = rev (Misc_Legacy.term_vars (Thm.concl_of case_thm));
- val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
+ val casethm_tvars = Misc_Legacy.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)))) =>