src/HOL/Tools/datatype_prop.ML
changeset 29270 0eade173f77e
parent 27300 4cb3101d2bf7
child 30190 479806475f3c
--- a/src/HOL/Tools/datatype_prop.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/datatype_prop.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Characteristic properties of datatypes.
@@ -206,7 +205,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
 
     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
 
@@ -256,7 +255,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
@@ -303,7 +302,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used' = foldr add_typ_tfree_names [] recTs;
+    val used' = foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);