--- a/src/Pure/Isar/isar_syn.ML Fri Feb 16 19:19:19 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Feb 16 22:13:15 2007 +0100
@@ -113,8 +113,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 fold AxClass.axiomatize_arity));
+ (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
(* consts and syntax *)
@@ -406,19 +405,13 @@
local
-val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
-
val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
-val parse_arity =
- (P.xname --| P.$$$ "::" -- P.!!! P.arity)
- >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
-
in
val classP =
- OuterSyntax.command classK "define type class" K.thy_decl (
+ OuterSyntax.command "class" "define type class" K.thy_decl (
P.name --| P.$$$ "="
-- (
class_subP --| P.$$$ "+" -- class_bodyP
@@ -430,17 +423,17 @@
(ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
val instanceP =
- OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
+ OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
>> ClassPackage.instance_class_cmd
|| P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
>> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
- || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
+ || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
>> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
) >> (Toplevel.print oo Toplevel.theory_to_proof));
val print_classesP =
- OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
+ OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));