1.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Mon Jul 05 16:43:08 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Tue Jul 06 09:21:13 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    lim  :: addr
     1.5  
     1.6  definition empty :: heap where
     1.7 -  "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" -- "why undefined?"
     1.8 +  "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
     1.9  
    1.10  datatype 'a array = Array addr
    1.11  datatype 'a ref = Ref addr -- "note the phantom type 'a "
    1.12 @@ -85,4 +85,6 @@
    1.13    #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
    1.14  *}
    1.15  
    1.16 +hide_const (open) empty
    1.17 +
    1.18  end