# 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;