src/HOL/Nominal/nominal_datatype.ML

--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:54:25 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 15:23:27 2011 +0100
@@ -1414,7 +1414,7 @@
 
     val _ = warning "defining recursion combinator ...";
 
-    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used = fold Term.add_tfree_namesT recTs [];
 
     val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;