src/ZF/Tools/inductive_package.ML

   val dummy = assert_all is_Free rec_params
       (fn t => "Param in recursion term not a free variable: " ^
                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";
 
   fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^