--- a/src/Pure/Isar/isar_syn.ML Fri May 21 21:20:14 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri May 21 21:20:38 2004 +0200
@@ -89,8 +89,8 @@
val classrelP =
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
- (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
- >> (Toplevel.theory o Theory.add_classrel o single));
+ (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
+ >> (Toplevel.theory o Theory.add_classrel));
val defaultsortP =
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl