src/Pure/Isar/isar_syn.ML
changeset 24748 ee0a0eb6b738
parent 24624 b8383b1bbae3
child 24830 a7b3ab44d993
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -415,14 +415,15 @@
     1.4    OuterSyntax.command "class" "define type class" K.thy_decl (
     1.5      P.name
     1.6      -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
     1.7 +    -- Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false
     1.8      --| P.$$$ "=" -- (
     1.9        class_subP --| P.$$$ "+" -- class_bodyP
    1.10        || class_subP >> rpair []
    1.11        || class_bodyP >> pair [])
    1.12      -- P.opt_begin
    1.13 -    >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
    1.14 +    >> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) =>
    1.15          Toplevel.begin_local_theory begin
    1.16 -          (Class.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
    1.17 +          (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin)));
    1.18  
    1.19  val instanceP =
    1.20    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
    1.21 @@ -985,7 +986,7 @@
    1.22    "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
    1.23    "constrains", "defines", "fixes", "for", "identifier", "if",
    1.24    "imports", "in", "includes", "infix", "infixl", "infixr", "is",
    1.25 -  "notes", "obtains", "open", "output", "overloaded", "shows",
    1.26 +  "local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows",
    1.27    "structure", "unchecked", "uses", "where", "|"];
    1.28  
    1.29  val _ = OuterSyntax.add_parsers [