local_theory: incorporated consts into axioms;
authorwenzelm
Thu Oct 11 21:10:40 2007 +0200 (2007-10-11 ago)
changeset 24984952045a8dcf2
parent 24983 f2f4ba67cef1
child 24985 0e5177e2c076
local_theory: incorporated consts into axioms;
src/Pure/Isar/instance.ML
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/instance.ML	Thu Oct 11 19:10:25 2007 +0200
     1.2 +++ b/src/Pure/Isar/instance.ML	Thu Oct 11 21:10:40 2007 +0200
     1.3 @@ -47,7 +47,6 @@
     1.4      val thy_target = TheoryTarget.begin "" ctxt;
     1.5      val operations = {
     1.6          pretty = LocalTheory.pretty,
     1.7 -        consts = LocalTheory.consts,
     1.8          axioms = LocalTheory.axioms,
     1.9          abbrev = LocalTheory.abbrev,
    1.10          def = LocalTheory.def,
     2.1 --- a/src/Pure/Isar/local_theory.ML	Thu Oct 11 19:10:25 2007 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Oct 11 21:10:40 2007 +0200
     2.3 @@ -21,10 +21,9 @@
     2.4    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     2.5    val affirm: local_theory -> local_theory
     2.6    val pretty: local_theory -> Pretty.T list
     2.7 -  val consts: (string * typ -> bool) ->
     2.8 -    ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
     2.9 -  val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
    2.10 -    (bstring * thm list) list * local_theory
    2.11 +  val axioms: string ->
    2.12 +    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    2.13 +    -> (term list * (bstring * thm list) list) * local_theory
    2.14    val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    2.15      (term * term) * local_theory
    2.16    val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
    2.17 @@ -55,10 +54,9 @@
    2.18  
    2.19  type operations =
    2.20   {pretty: local_theory -> Pretty.T list,
    2.21 -  consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory ->
    2.22 -    (term * thm) list * local_theory,
    2.23 -  axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
    2.24 -    (bstring * thm list) list * local_theory,
    2.25 +  axioms: string ->
    2.26 +    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    2.27 +    -> (term list * (bstring * thm list) list) * local_theory,
    2.28    abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
    2.29    def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
    2.30      local_theory -> (term * (bstring * thm)) * local_theory,
    2.31 @@ -151,7 +149,6 @@
    2.32  fun operation2 f x y = operation (fn ops => f ops x y);
    2.33  
    2.34  val pretty = operation #pretty;
    2.35 -val consts = operation2 #consts;
    2.36  val axioms = operation2 #axioms;
    2.37  val abbrev = operation2 #abbrev;
    2.38  val def = operation2 #def;