src/Pure/Isar/isar_syn.ML
changeset 22385 cc2be3315e72
parent 22351 587845efb4cf
child 22415 c310ca7cd47f
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 02 15:43:15 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 02 15:43:16 2007 +0100
     1.3 @@ -88,9 +88,8 @@
     1.4    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     1.5      (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     1.6          P.!!! (P.list1 P.xname)) []
     1.7 -        -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
     1.8          -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
     1.9 -      >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    1.10 +      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
    1.11  
    1.12  
    1.13  (* types *)
    1.14 @@ -412,15 +411,16 @@
    1.15  
    1.16  val classP =
    1.17    OuterSyntax.command "class" "define type class" K.thy_decl (
    1.18 -    P.name --| P.$$$ "="
    1.19 -    -- (
    1.20 +    P.name
    1.21 +    -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
    1.22 +    --| P.$$$ "=" -- (
    1.23        class_subP --| P.$$$ "+" -- class_bodyP
    1.24        || class_subP >> rpair []
    1.25        || class_bodyP >> pair [])
    1.26      -- P.opt_begin
    1.27 -    >> (fn ((bname, (supclasses, elems)), begin) =>
    1.28 +    >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
    1.29          Toplevel.begin_local_theory begin
    1.30 -          (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin)));
    1.31 +          (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
    1.32  
    1.33  val instanceP =
    1.34    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((