# HG changeset patch
# User wenzelm
# Date 1166017950 -3600
# Node ID d7bb902beb07387ce2f740ecb11985ef05611c57
# Parent  06a06f6d3166eeb2e24d513221df2cebe3db70f4
local_abbrev: proper fix/declare of local entities;

diff -r 06a06f6d3166 -r d7bb902beb07 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Dec 13 12:42:26 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Dec 13 14:52:30 2006 +0100
@@ -921,10 +921,16 @@
   end;
 
 fun local_abbrev (x, rhs) =
-  let
-    val T = Term.fastype_of rhs;
-    val export = Envir.expand_term_frees [((x, T), rhs)];
-  in Assumption.add_assms (K (K (I, export))) [] #> snd #> pair (Free (x, T), rhs) end;
+  Variable.add_fixes [x] #-> (fn [x'] =>
+    let
+      val T = Term.fastype_of rhs;
+      val lhs = Free (x', T);
+    in
+      Variable.declare_term lhs #>
+      Variable.declare_term rhs #>
+      Assumption.add_assms (K (K (I, Envir.expand_term_frees [((x', T), rhs)]))) [] #> snd #>
+      pair (lhs, rhs)
+    end);
 
 
 (* fixes *)