1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 11 16:53:23 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 11 16:53:27 2006 +0100
     1.3 @@ -89,6 +89,12 @@
     1.4    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     1.5      (P.sort >> (Toplevel.theory o Theory.add_defsort));
     1.6  
     1.7 +val axclassP =
     1.8 +  OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     1.9 +    ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    1.10 +        P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
    1.11 +      >> (Toplevel.theory o (snd oo uncurry AxClass.add_axclass)));
    1.12 +
    1.13  
    1.14  (* types *)
    1.15  
    1.16 @@ -867,9 +873,9 @@
    1.17    headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
    1.18    text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
    1.19    (*theory sections*)
    1.20 -  classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
    1.21 -  aritiesP, judgmentP, constsP, finalconstsP, syntaxP, no_syntaxP,
    1.22 -  translationsP, axiomsP, defsP, constdefsP, definitionP,
    1.23 +  classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
    1.24 +  nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
    1.25 +  no_syntaxP, translationsP, axiomsP, defsP, constdefsP, definitionP,
    1.26    abbreviationP, axiomatizationP, theoremsP, lemmasP, declareP,
    1.27    globalP, localP, hideP, useP, mlP, ml_commandP, ml_setupP, setupP,
    1.28    method_setupP, parse_ast_translationP, parse_translationP,