# HG changeset patch
# User haftmann
# Date 1207144718 -7200
# Node ID 1bf210ac0a90cc47997f6146c393bd2fcf6f7687
# Parent  4a2063a8c2d209d3a9de70116bc411503529c50b
removed obscure "attach" feature

diff -r 4a2063a8c2d2 -r 1bf210ac0a90 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Wed Apr 02 15:58:37 2008 +0200
+++ b/src/Pure/Isar/instance.ML	Wed Apr 02 15:58:38 2008 +0200
@@ -47,18 +47,18 @@
       in Specification.definition def' ctxt end;
     val _ = if not (null defs) then Output.legacy_feature
       "Instance command with attached definitions; use instantiation instead." else ();
-  in if not (null defs) orelse forall (Class.is_class thy) sort
+  in if null defs
   then
     thy
+    |> Class.instance_arity I (tyco, map snd vs, sort)
+  else
+    thy
     |> TheoryTarget.instantiation ([tyco], vs, sort)
     |> `(fn ctxt => map (mk_def ctxt) defs)
     |-> (fn defs => fold_map Specification.definition defs)
     |> snd
     |> LocalTheory.restore
     |> Class.instantiation_instance Class.conclude_instantiation
-  else
-    thy
-    |> Class.instance_arity I (tyco, map snd vs, sort)
   end;
 
 end;
diff -r 4a2063a8c2d2 -r 1bf210ac0a90 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 02 15:58:37 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 02 15:58:38 2008 +0200
@@ -433,12 +433,10 @@
 
 val _ =
   OuterSyntax.command "class" "define type class" K.thy_decl
-   (P.name --
-     Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] --  (* FIXME ?? *)
-     (P.$$$ "=" |-- class_val) -- P.opt_begin
-    >> (fn (((name, add_consts), (supclasses, elems)), begin) =>
+   (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
+    >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-          (Class.class_cmd name supclasses elems add_consts #-> TheoryTarget.begin)));
+          (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
 
 val _ =
   OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal
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;