--- a/src/HOL/Word/WordShift.thy Sat May 17 23:37:09 2008 +0200
+++ b/src/HOL/Word/WordShift.thy Sat May 17 23:37:11 2008 +0200
@@ -1541,7 +1541,7 @@
lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
-lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map
+lemmas ths_map [where xs = "to_bl v", standard] = rotate_map rotater_map
lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
--- a/src/HOLCF/ex/Hoare.thy Sat May 17 23:37:09 2008 +0200
+++ b/src/HOLCF/ex/Hoare.thy Sat May 17 23:37:11 2008 +0200
@@ -158,7 +158,7 @@
(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
-thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard, no_vars]
+thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
lemma hoare_lemma10:
"EX k. b1$(iterate k$g$x) ~= TT