# HG changeset patch
# User wenzelm
# Date 949945193 -3600
# Node ID b2a4a3d86b731e09224c69abcd2c23bbdef0eadf
# Parent  2fcc6017cb72bbfb2cb9075b41ba76d462d7bb8c
tuned prefer/defer;

diff -r 2fcc6017cb72 -r b2a4a3d86b73 src/Pure/Isar/isar_thy.ML
--- 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 *)