--- 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 *))