diff -r 98744e38ded1 -r 22081de41254 src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Fri Oct 23 20:34:59 1998 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML	Fri Oct 23 20:35:19 1998 +0200
@@ -64,7 +64,7 @@
 
 qed_goal "MemReturn_change" Memory.thy
    "MemReturn ch rs p .-> <MemReturn ch rs p>_<rtrner ch @ p, rs@p>"
-   (fn _ => [ auto_tac (action_css addsimps2 [MemReturn_def,angle_def]) ]);
+   (K [ force_tac (action_css addsimps2 [MemReturn_def,angle_def]) 1]);
 
 qed_goal "MemReturn_enabled" Memory.thy
    "!!p. base_var <rtrner ch @ p, rs@p> ==> \