# HG changeset patch
# User wenzelm
# Date 1085167238 -7200
# Node ID e15d4bd7fe717bd703589febe2645a2261cde6eb
# Parent  69cafc301399f93307e4eb58d68f36ecf256f885
'classrel' now allows multiple arguments;

diff -r 69cafc301399 -r e15d4bd7fe71 src/Pure/Isar/isar_syn.ML
--- 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