src/Pure/logic.ML

   in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
 
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
+  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (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]);