# HG changeset patch
# User wenzelm
# Date 1140110761 -3600
# Node ID c36eb33c84289e703a8f622f030ac4bf77fc098b
# Parent  e1948ebe9c7d24b0baff76672921a1a8d41f1a43
added abbrev element;

diff -r e1948ebe9c7d -r c36eb33c8428 src/Pure/Isar/local_theory.ML
--- 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;