# HG changeset patch
# User wenzelm
# Date 1192129840 -7200
# Node ID 952045a8dcf22125731a5a2b84b8589a6c57ff88
# Parent  f2f4ba67cef18410e3f3b7ade875b61f55fd1e3c
local_theory: incorporated consts into axioms;

diff -r f2f4ba67cef1 -r 952045a8dcf2 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Thu Oct 11 19:10:25 2007 +0200
+++ b/src/Pure/Isar/instance.ML	Thu Oct 11 21:10:40 2007 +0200
@@ -47,7 +47,6 @@
     val thy_target = TheoryTarget.begin "" ctxt;
     val operations = {
         pretty = LocalTheory.pretty,
-        consts = LocalTheory.consts,
         axioms = LocalTheory.axioms,
         abbrev = LocalTheory.abbrev,
         def = LocalTheory.def,
diff -r f2f4ba67cef1 -r 952045a8dcf2 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Oct 11 19:10:25 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Oct 11 21:10:40 2007 +0200
@@ -21,10 +21,9 @@
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
-  val consts: (string * typ -> bool) ->
-    ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
-  val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
-    (bstring * thm list) list * local_theory
+  val axioms: string ->
+    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
+    -> (term list * (bstring * thm list) list) * local_theory
   val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
@@ -55,10 +54,9 @@
 
 type operations =
  {pretty: local_theory -> Pretty.T list,
-  consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory ->
-    (term * thm) list * local_theory,
-  axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
-    (bstring * thm list) list * local_theory,
+  axioms: string ->
+    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
+    -> (term list * (bstring * thm list) list) * local_theory,
   abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
   def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     local_theory -> (term * (bstring * thm)) * local_theory,
@@ -151,7 +149,6 @@
 fun operation2 f x y = operation (fn ops => f ops x y);
 
 val pretty = operation #pretty;
-val consts = operation2 #consts;
 val axioms = operation2 #axioms;
 val abbrev = operation2 #abbrev;
 val def = operation2 #def;