src/ZF/Tools/inductive_package.ML

--- a/src/ZF/Tools/inductive_package.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -96,7 +96,7 @@
                Syntax.string_of_term ctxt t);
 
   (*** Construct the fixedpoint definition ***)
-  val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
+  val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";