src/Pure/Isar/isar_syn.ML
changeset 22331 7df6bc8cf0b0
parent 22321 e5cddafe2629
child 22340 275802767bf3
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Feb 16 19:19:19 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 16 22:13:15 2007 +0100
     1.3 @@ -113,8 +113,7 @@
     1.4  
     1.5  val aritiesP =
     1.6    OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
     1.7 -    (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
     1.8 -      >> (Toplevel.theory o fold AxClass.axiomatize_arity));
     1.9 +    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
    1.10  
    1.11  
    1.12  (* consts and syntax *)
    1.13 @@ -406,19 +405,13 @@
    1.14  
    1.15  local
    1.16  
    1.17 -val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
    1.18 -
    1.19  val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
    1.20  val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
    1.21  
    1.22 -val parse_arity =
    1.23 -  (P.xname --| P.$$$ "::" -- P.!!! P.arity)
    1.24 -    >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
    1.25 -
    1.26  in
    1.27  
    1.28  val classP =
    1.29 -  OuterSyntax.command classK "define type class" K.thy_decl (
    1.30 +  OuterSyntax.command "class" "define type class" K.thy_decl (
    1.31      P.name --| P.$$$ "="
    1.32      -- (
    1.33        class_subP --| P.$$$ "+" -- class_bodyP
    1.34 @@ -430,17 +423,17 @@
    1.35            (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
    1.36  
    1.37  val instanceP =
    1.38 -  OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    1.39 +  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
    1.40        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.41             >> ClassPackage.instance_class_cmd
    1.42        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.43             >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
    1.44 -      || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.45 +      || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.46             >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
    1.47      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.48  
    1.49  val print_classesP =
    1.50 -  OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
    1.51 +  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
    1.52      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
    1.53        o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
    1.54