--- a/src/Pure/Isar/isar_thy.ML Mon Feb 07 18:38:51 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML Mon Feb 07 18:39:53 2000 +0100
@@ -346,8 +346,10 @@
(* shuffle state *)
-fun defer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.defer i))));
-fun prefer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.prefer i))));
+fun shuffle meth i = Method.refine_no_facts (Method.Basic (K (meth i))) o Proof.assert_no_chain;
+
+fun defer i = ProofHistory.applys (shuffle Method.defer i);
+fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
(* backward steps *)