--- 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)));