# HG changeset patch
# User wenzelm
# Date 1192899273 -7200
# Node ID 192105867f2540255d4c73bf36d1c36bda212556
# Parent  158149a6e95b322ca7d35646a9ac5ac8df690f0b
added fixed_abbrev;

diff -r 158149a6e95b -r 192105867f25 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Oct 20 18:54:31 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat Oct 20 18:54:33 2007 +0200
@@ -15,6 +15,7 @@
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
   val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+  val fixed_abbrev: (string * mixfix) * term -> Proof.context -> (term * term) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> thm list * thm
   val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
   val trans_terms: Proof.context -> thm list -> thm
@@ -106,6 +107,21 @@
   in ((lhs, th), ctxt') end;
 
 
+(* fixed_abbrev *)
+
+fun fixed_abbrev ((x, mx), rhs) ctxt =
+  let
+    val T = Term.fastype_of rhs;
+    val ([x'], ctxt') = ctxt
+      |> Variable.declare_term rhs
+      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
+    val lhs = Free (x', T);
+    val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
+    fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
+    val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
+  in ((lhs, rhs), ctxt'') end;
+
+
 (* specific export -- result based on educated guessing *)
 
 (*