diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/TFL/casesplit.ML
-    ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 A structure that defines a tactic to program case splits.
@@ -104,7 +103,7 @@
     end;
 
 (*
- val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
+ val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
 *)
 
 
@@ -122,7 +121,7 @@
       val abs_ct = ctermify abst;
       val free_ct = ctermify x;
 
-      val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
+      val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
 
       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
       val (Pv, Dv, type_insts) =
@@ -170,7 +169,7 @@
       val subgoalth' = atomize_goals subgoalth;
       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
 
-      val freets = Term.term_frees gt;
+      val freets = OldTerm.term_frees gt;
       fun getter x =
           let val (n,ty) = Term.dest_Free x in
             (if vstr = n orelse vstr = Name.dest_skolem n