src/Pure/axclass.ML

     val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
 
     val binding =
       Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
 
-    val args = Name.invent_types_global Ss;
+    val args = map TFree (Name.invent_types_global Ss);
     val missing_params =
       Sign.complete_sort thy [c]
       |> maps (these o Option.map #params o try (get_info thy))
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
-      |> (map o apsnd o map_atyps) (K (Type (t, map TFree args)));
+      |> (map o apsnd o map_atyps) (K (Type (t, args)));
   in
     thy
     |> Global_Theory.store_thm (binding, th)
     |-> Thm.add_arity
     |> fold (#2 oo declare_overloaded) missing_params