diff -r 373727835757 -r 40f414b87655 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Jul 30 19:46:13 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Jul 30 19:46:15 2007 +0200
@@ -127,7 +127,8 @@
 abbreviation "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
 abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
 
-ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
+lemmas map_of_Cons = map_of.simps(2)
+
 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
 apply (simp (no_asm))
 done