# HG changeset patch
# User wenzelm
# Date 927575598 -7200
# Node ID 7c2dafc8e8013ff79b778dff2c7f67138df563de
# Parent  e869ff059252fa4ed1a1b80bd01f9968d7524923
outer syntax keyword classification;
no open OuterParse;

diff -r e869ff059252 -r 7c2dafc8e801 src/Pure/axclass.ML
--- 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];