diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/Example.thy	Wed Mar 25 10:44:57 2015 +0100
@@ -1259,18 +1259,18 @@
 apply (simp (no_asm_use))
 apply (drule (1) alloc_one,clarsimp)
 apply (rule eval_Is (* ;; *))
-apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
-apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
-apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
+apply  (erule_tac V = "the (new_Addr _) = c" in thin_rl)
+apply  (erule_tac [2] V = "new_Addr _ = Some a" in thin_rl)
+apply  (erule_tac [2] V = "atleast_free _ four" in thin_rl)
 apply  (rule eval_Is (* Expr *))
 apply  (rule eval_Is (* Ass *))
 apply   (rule eval_Is (* LVar *))
 apply  (rule eval_Is (* NewC *))
       (* begin init Ext *)
-apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
-apply   (erule_tac V = "atleast_free ?h three" in thin_rl)
-apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
-apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
+apply   (erule_tac V = "the (new_Addr _) = b" in thin_rl)
+apply   (erule_tac V = "atleast_free _ three" in thin_rl)
+apply   (erule_tac [2] V = "atleast_free _ four" in thin_rl)
+apply   (erule_tac [2] V = "new_Addr _ = Some a" in thin_rl)
 apply   (rule eval_Is (* Init Ext *))
 apply   (simp)
 apply   (rule conjI)
@@ -1309,7 +1309,7 @@
 apply (drule alloc_one)
 apply  (simp (no_asm_simp))
 apply clarsimp
-apply (erule_tac V = "atleast_free ?h three" in thin_rl)
+apply (erule_tac V = "atleast_free _ three" in thin_rl)
 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
 apply (simp (no_asm_use))
 apply (rule eval_Is (* Try *))
@@ -1361,7 +1361,7 @@
 apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
 apply (drule alloc_one [THEN conjunct1])
 apply  (simp (no_asm_simp))
-apply (erule_tac V = "atleast_free ?h two" in thin_rl)
+apply (erule_tac V = "atleast_free _ two" in thin_rl)
 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
 apply simp
 apply (rule eval_Is (* While *))