# HG changeset patch
# User haftmann
# Date 1138899815 -3600
# Node ID 74edab16166fd2356ad426ba72ef6e62801760b3
# Parent  50a27d7c8951d57e8a90052d72b878bd9773715e
alternative syntax for instances

diff -r 50a27d7c8951 -r 74edab16166f src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Thu Feb 02 16:37:10 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Thu Feb 02 18:03:35 2006 +0100
@@ -506,6 +506,13 @@
 
 val (classK, instanceK) = ("class", "instance")
 
+val parse_inst =
+  P.xname -- (
+    Scan.repeat P.sort --| P.$$$ "::" -- P.sort
+    || P.$$$ "::" |-- P.!!! P.arity
+  )
+  >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort))
+
 val classP =
   OuterSyntax.command classK "operational type classes" K.thy_decl (
     P.name --| P.$$$ "="
@@ -517,9 +524,9 @@
 val instanceP =
   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
-      || P.xname -- (P.$$$ "::" |-- P.!!! P.arity) -- Scan.repeat P.spec_name
-           >> (fn ((tyco, (asorts, sort)), []) => AxClass.instance_arity I (tyco, asorts, sort)
-                | ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs)
+      || parse_inst -- Scan.repeat P.spec_name
+           >> (fn (((tyco, asorts), sort), []) => AxClass.instance_arity I (tyco, asorts, sort)
+                | (inst, defs) => add_instance_arity inst defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val _ = OuterSyntax.add_parsers [classP, instanceP];