src/Pure/logic.ML

 
 
 (* type arities *)
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss))
+  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
   in map (fn c => mk_inclass (T, c)) S end;
 
 fun dest_arity tm =
   let
     fun err () = raise TERM ("dest_arity", [tm]);

   if n>0 then deletes assumption n. *)
 fun flatten_params n A =
     let val params = strip_params A;
         val vars = if !auto_rename
                    then rename_vars (!rename_prefix, params)
-                   else ListPair.zip (variantlist(map #1 params,[]),
+                   else ListPair.zip (Name.variant_list [] (map #1 params),
                                       map #2 params)
     in  list_all (vars, remove_params (length vars) n A)
     end;
 
 (*Makes parameters in a goal have the names supplied by the list cs.*)