--- a/src/Pure/axclass.ML Mon May 24 15:56:24 1999 +0200
+++ b/src/Pure/axclass.ML Mon May 24 21:53:18 1999 +0200
@@ -426,17 +426,17 @@
(* outer syntax *)
-local open OuterParse in
+local structure P = OuterParse and K = OuterSyntax.Keyword in
val axclassP =
- OuterSyntax.command "axclass" "define axiomatic type class"
- (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [] -- Scan.repeat spec_name
+ OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
+ (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [] -- Scan.repeat P.spec_name
>> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
val instanceP =
- OuterSyntax.command "instance" "prove type arity or subclass relation"
- ((xname -- ($$$ "<" |-- xname) >> instance_subclass_proof ||
- xname -- ($$$ "::" |-- simple_arity) >> (instance_arity_proof o triple2))
+ OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
+ ((P.xname -- (P.$$$ "<" |-- P.xname) >> instance_subclass_proof ||
+ P.xname -- (P.$$$ "::" |-- P.simple_arity) >> (instance_arity_proof o P.triple2))
>> (Toplevel.print oo Toplevel.theory_to_proof));
val _ = OuterSyntax.add_parsers [axclassP, instanceP];