# HG changeset patch
# User wenzelm
# Date 1146430210 -7200
# Node ID dcc4b1d5b73220d0333ad5fa5d6eebd798328647
# Parent  9f650083da65729483142627648ea35f158ac937
AxClass.define_class;
AxClass.axiomatize_class/classrel/arity;

diff -r 9f650083da65 -r dcc4b1d5b732 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 30 22:50:09 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 30 22:50:10 2006 +0200
@@ -78,12 +78,12 @@
 val classesP =
   OuterSyntax.command "classes" "declare type classes" K.thy_decl
     (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
-        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o Theory.add_classes));
+        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class));
 
 val classrelP =
   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
     (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
-    >> (Toplevel.theory o Theory.add_classrel));
+    >> (Toplevel.theory o AxClass.axiomatize_classrel));
 
 val defaultsortP =
   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
@@ -94,7 +94,7 @@
     ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         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)));
+      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
 
 
 (* types *)
@@ -118,7 +118,7 @@
 val aritiesP =
   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
     (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
-      >> (Toplevel.theory o Theory.add_arities));
+      >> (Toplevel.theory o fold AxClass.axiomatize_arity));
 
 
 (* consts and syntax *)