src/Pure/Isar/isar_thy.ML
changeset 8204 b2a4a3d86b73
parent 8165 651b006d7eb8
child 8210 ca3997312f47
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Feb 07 18:38:51 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Feb 07 18:39:53 2000 +0100
     1.3 @@ -346,8 +346,10 @@
     1.4  
     1.5  (* shuffle state *)
     1.6  
     1.7 -fun defer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.defer i))));
     1.8 -fun prefer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.prefer i))));
     1.9 +fun shuffle meth i = Method.refine_no_facts (Method.Basic (K (meth i))) o Proof.assert_no_chain;
    1.10 +
    1.11 +fun defer i = ProofHistory.applys (shuffle Method.defer i);
    1.12 +fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
    1.13  
    1.14  
    1.15  (* backward steps *)