--- a/src/Pure/Isar/local_theory.ML Thu Feb 16 18:26:00 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML Thu Feb 16 18:26:01 2006 +0100
@@ -41,6 +41,7 @@
val def_finish: (local_theory -> term -> thm -> thm) ->
(bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
local_theory -> (term * (bstring * thm)) * local_theory
+ val abbrev: bool -> (bstring * mixfix) * term -> local_theory -> local_theory
end;
structure LocalTheory: LOCAL_THEORY =
@@ -276,4 +277,18 @@
end;
+
+(* constant abbreviations *)
+
+fun abbrev revert ((x, mx), rhs) ctxt =
+ let val abbrevs = [(x, rhs, mx)] in
+ ctxt |>
+ (case locale_of ctxt of
+ NONE =>
+ theory (Sign.add_abbrevs_i revert abbrevs)
+ | SOME (loc, _) =>
+ locale (Locale.add_abbrevs loc revert abbrevs) #>
+ ProofContext.add_abbrevs_i revert abbrevs)
+ end;
+
end;