src/Pure/Isar/isar_syn.ML
changeset 24932 86ef9a828a9e
parent 24914 95cda5dd58d5
child 24938 a220317465b4
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 09 17:10:44 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 09 17:10:45 2007 +0200
     1.3 @@ -89,12 +89,12 @@
     1.4  val _ =
     1.5    OuterSyntax.command "classes" "declare type classes" K.thy_decl
     1.6      (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     1.7 -        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class));
     1.8 +        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    1.12      (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
    1.13 -    >> (Toplevel.theory o AxClass.axiomatize_classrel));
    1.14 +    >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
    1.15  
    1.16  val _ =
    1.17    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    1.18 @@ -128,7 +128,7 @@
    1.19  
    1.20  val _ =
    1.21    OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
    1.22 -    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
    1.23 +    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
    1.24  
    1.25  
    1.26  (* consts and syntax *)
    1.27 @@ -234,19 +234,19 @@
    1.28  val _ =
    1.29    OuterSyntax.command "definition" "constant definition" K.thy_decl
    1.30      (P.opt_target -- constdef
    1.31 -    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
    1.32 +    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition_cmd args)));
    1.33  
    1.34  val _ =
    1.35    OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
    1.36      (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
    1.37      >> (fn ((loc, mode), args) =>
    1.38 -        Toplevel.local_theory loc (Specification.abbreviation mode args)));
    1.39 +        Toplevel.local_theory loc (Specification.abbreviation_cmd mode args)));
    1.40  
    1.41  val _ =
    1.42    OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
    1.43      (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    1.44      >> (fn ((loc, mode), args) =>
    1.45 -        Toplevel.local_theory loc (Specification.notation mode args)));
    1.46 +        Toplevel.local_theory loc (Specification.notation_cmd mode args)));
    1.47  
    1.48  
    1.49  (* constant specifications *)
    1.50 @@ -256,13 +256,13 @@
    1.51      (P.opt_target --
    1.52       (Scan.optional P.fixes [] --
    1.53        Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
    1.54 -    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
    1.55 +    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization_cmd x y)));
    1.56  
    1.57  
    1.58  (* theorems *)
    1.59  
    1.60  fun theorems kind = P.opt_target -- SpecParse.name_facts
    1.61 -  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
    1.62 +  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems_cmd kind args));
    1.63  
    1.64  val _ =
    1.65    OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
    1.66 @@ -274,7 +274,7 @@
    1.67    OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl
    1.68      (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
    1.69        >> (fn (loc, args) => Toplevel.local_theory loc
    1.70 -          (#2 o Specification.theorems "" [(("", []), args)])));
    1.71 +          (#2 o Specification.theorems_cmd "" [(("", []), args)])));
    1.72  
    1.73  
    1.74  (* name space entry path *)
    1.75 @@ -381,7 +381,7 @@
    1.76  val _ =
    1.77    OuterSyntax.command "context" "enter local theory context" K.thy_decl
    1.78      (P.name --| P.begin >> (fn name =>
    1.79 -      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
    1.80 +      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd (SOME name))));
    1.81  
    1.82  
    1.83  (* locales *)
    1.84 @@ -476,7 +476,7 @@
    1.85        SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
    1.86        (Toplevel.print o
    1.87         Toplevel.local_theory_to_proof' loc
    1.88 -         (Specification.theorem kind NONE (K I) a elems concl))));
    1.89 +         (Specification.theorem_cmd kind NONE (K I) a elems concl))));
    1.90  
    1.91  val _ = gen_theorem Thm.theoremK;
    1.92  val _ = gen_theorem Thm.lemmaK;