outer syntax keyword classification;
authorwenzelm
Mon May 24 21:53:18 1999 +0200 (1999-05-24)
changeset 67197c2dafc8e801
parent 6718 e869ff059252
child 6720 353bd9b74b1f
outer syntax keyword classification;
no open OuterParse;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Mon May 24 15:56:24 1999 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon May 24 21:53:18 1999 +0200
     1.3 @@ -426,17 +426,17 @@
     1.4  
     1.5  (* outer syntax *)
     1.6  
     1.7 -local open OuterParse in
     1.8 +local structure P = OuterParse and K = OuterSyntax.Keyword in
     1.9  
    1.10  val axclassP =
    1.11 -  OuterSyntax.command "axclass" "define axiomatic type class"
    1.12 -    (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [] -- Scan.repeat spec_name
    1.13 +  OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    1.14 +    (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [] -- Scan.repeat P.spec_name
    1.15        >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
    1.16  
    1.17  val instanceP =
    1.18 -  OuterSyntax.command "instance" "prove type arity or subclass relation"
    1.19 -    ((xname -- ($$$ "<" |-- xname) >> instance_subclass_proof ||
    1.20 -      xname -- ($$$ "::" |-- simple_arity) >> (instance_arity_proof o triple2))
    1.21 +  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.22 +    ((P.xname -- (P.$$$ "<" |-- P.xname) >> instance_subclass_proof ||
    1.23 +      P.xname -- (P.$$$ "::" |-- P.simple_arity) >> (instance_arity_proof o P.triple2))
    1.24        >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.25  
    1.26  val _ = OuterSyntax.add_parsers [axclassP, instanceP];