diff -r 4a2063a8c2d2 -r 1bf210ac0a90 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 02 15:58:37 2008 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 02 15:58:38 2008 +0200
@@ -258,35 +258,14 @@
     val prop = Thm.plain_prop_of (Thm.transfer thy th);
     val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
     val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
-    (*FIXME turn this into a mere check as soon as "attach" has disappeared*)
-    val missing_params = Sign.complete_sort thy [c]
-      |> maps (these o Option.map (fn AxClass { params, ... } => params) o lookup_def thy)
-      |> filter_out (fn (p, _) => can (get_inst_param thy) (p, t));
-    fun declare_missing (p, T0) thy =
-      let
-        val name_inst = instance_name (t, c) ^ "_inst";
-        val p' = NameSpace.base p ^ "_" ^ NameSpace.base t;
-        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy t) []);
-        val T = map_atyps (fn _ => Type (t, map TFree vs)) T0;
-      in
-        thy
-        |> Sign.sticky_prefix name_inst
-        |> Sign.no_base_names
-        |> Sign.declare_const [] (p', T, NoSyn)
-        |-> (fn const' as Const (p'', _) => Thm.add_def false true
-              (Thm.def_name p', Logic.mk_equals (const', Const (p, T)))
-        #>> Thm.varifyT
-        #-> (fn thm => add_inst_param (p, t) (p'', Thm.symmetric thm)
-        #> PureThy.note Thm.internalK (p', thm)
-        #> snd
-        #> Sign.restore_naming thy))
-      end;
-
+    val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c)
+     of [] => ()
+      | cs => Output.legacy_feature
+          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])
     |> put_arity ((t, Ss, c), Drule.unconstrainTs th)
-    |> fold declare_missing missing_params
   end;