--- a/src/Pure/Isar/isar_syn.ML Fri Dec 29 19:50:52 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Dec 29 20:34:17 2006 +0100
@@ -88,7 +88,7 @@
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
(P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
P.!!! (P.list1 P.xname)) []
- -- Scan.optional (P.$$$ "attach" |-- Scan.repeat P.term) []
+ -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
-- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
>> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));