--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Nov 20 21:05:23 2011 +0100
@@ -819,7 +819,7 @@
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
-lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard]
+lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"