# HG changeset patch
# User kleing
# Date 1307467372 -7200
# Node ID c729110a9f087c62c504fb29b6524d63dd86ea21
# Parent  6c3a2c33fc3934e4326e84183fff8e9338a6a785
use null_heap instead of %_. 0 to avoid printing problems

diff -r 6c3a2c33fc39 -r c729110a9f08 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Tue Jun 07 14:38:42 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Tue Jun 07 19:22:52 2011 +0200
@@ -35,17 +35,20 @@
 syntax (xsymbols)
   "_funlet"  :: "['a, 'a] => funlet"             ("_ /\<rightarrow>/ _")
 
+definition
+  "null_heap \<equiv> \<lambda>x. 0"
+
 translations
   "_FunUpd m (_Funlets xy ms)"  == "_FunUpd (_FunUpd m xy) ms"
   "_FunUpd m (_funlet  x y)"    == "m(x := y)"
-  "_Fun ms"                     == "_FunUpd (%_. 0) ms"
+  "_Fun ms"                     == "_FunUpd (CONST null_heap) ms"
   "_Fun (_Funlets ms1 ms2)"     <= "_FunUpd (_Fun ms1) ms2"
   "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3"
 
 text {* 
   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
 *}
-lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = ((%_. 0) (a := Suc 0)) (b := 2)"
+lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = (null_heap (a := Suc 0)) (b := 2)"
   by (rule refl)
 
 value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 7]"