src/Pure/Isar/isar_syn.ML
changeset 26516 1bf210ac0a90
parent 26490 87d27e426f14
child 26619 c348bbe7c87d
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 02 15:58:37 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 02 15:58:38 2008 +0200
     1.3 @@ -433,12 +433,10 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.command "class" "define type class" K.thy_decl
     1.7 -   (P.name --
     1.8 -     Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] --  (* FIXME ?? *)
     1.9 -     (P.$$$ "=" |-- class_val) -- P.opt_begin
    1.10 -    >> (fn (((name, add_consts), (supclasses, elems)), begin) =>
    1.11 +   (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
    1.12 +    >> (fn ((name, (supclasses, elems)), begin) =>
    1.13          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    1.14 -          (Class.class_cmd name supclasses elems add_consts #-> TheoryTarget.begin)));
    1.15 +          (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
    1.16  
    1.17  val _ =
    1.18    OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal