diff -r 177e35232d1b -r 20e86336a53f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 13 12:01:08 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 13 12:01:09 2006 +0200
@@ -92,7 +92,8 @@
 val axclassP =
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
-        P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
+        P.!!! (P.list1 P.xname)) []) --
+          Scan.repeat (P.thm_name ":" -- (P.prop >> single))
       >> (fn (x, y) => Toplevel.theory (snd o AxClass.add_axclass x [] y)));