# 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 *)