# HG changeset patch
# User wenzelm
# Date 1191942645 -7200
# Node ID 86ef9a828a9e9877c0dbacdb57e95717eb418c1b
# Parent  e0a2c154df261f80cee4722fa136fe6e7408aa09
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;

diff -r e0a2c154df26 -r 86ef9a828a9e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 09 17:10:44 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 09 17:10:45 2007 +0200
@@ -89,12 +89,12 @@
 val _ =
   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 fold AxClass.axiomatize_class));
+        P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
   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 AxClass.axiomatize_classrel));
+    >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
@@ -128,7 +128,7 @@
 
 val _ =
   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
-    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
+    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
 
 
 (* consts and syntax *)
@@ -234,19 +234,19 @@
 val _ =
   OuterSyntax.command "definition" "constant definition" K.thy_decl
     (P.opt_target -- constdef
-    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
+    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition_cmd args)));
 
 val _ =
   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
     (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
     >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.abbreviation mode args)));
+        Toplevel.local_theory loc (Specification.abbreviation_cmd mode args)));
 
 val _ =
   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
     (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.notation mode args)));
+        Toplevel.local_theory loc (Specification.notation_cmd mode args)));
 
 
 (* constant specifications *)
@@ -256,13 +256,13 @@
     (P.opt_target --
      (Scan.optional P.fixes [] --
       Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
-    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
+    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization_cmd x y)));
 
 
 (* theorems *)
 
 fun theorems kind = P.opt_target -- SpecParse.name_facts
-  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
+  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems_cmd kind args));
 
 val _ =
   OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
@@ -274,7 +274,7 @@
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl
     (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
       >> (fn (loc, args) => Toplevel.local_theory loc
-          (#2 o Specification.theorems "" [(("", []), args)])));
+          (#2 o Specification.theorems_cmd "" [(("", []), args)])));
 
 
 (* name space entry path *)
@@ -381,7 +381,7 @@
 val _ =
   OuterSyntax.command "context" "enter local theory context" K.thy_decl
     (P.name --| P.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
+      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd (SOME name))));
 
 
 (* locales *)
@@ -476,7 +476,7 @@
       SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
       (Toplevel.print o
        Toplevel.local_theory_to_proof' loc
-         (Specification.theorem kind NONE (K I) a elems concl))));
+         (Specification.theorem_cmd kind NONE (K I) a elems concl))));
 
 val _ = gen_theorem Thm.theoremK;
 val _ = gen_theorem Thm.lemmaK;