src/Pure/Isar/local_theory.ML

   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
-  val axioms: string ->
-    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory
-    -> (term list * (string * thm list) list) * local_theory
   val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory

 
 (* type lthy *)
 
 type operations =
  {pretty: local_theory -> Pretty.T list,
-  axioms: string ->
-    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory ->
-    (term list * (string * thm list) list) * local_theory,
   abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   define: string ->
     (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,

 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
 fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
 
 val pretty = operation #pretty;
-val axioms = operation2 #axioms;
 val abbrev = operation2 #abbrev;
 val define = operation2 #define;
 val notes = operation2 #notes;
 val type_syntax = operation1 #type_syntax;
 val term_syntax = operation1 #term_syntax;