proof step: reset goal_facts;
authorwenzelm
Mon Feb 14 20:42:02 2000 +0100 (2000-02-14)
changeset 8242ac8ac0eba738
parent 8241 a55484a9b19f
child 8243 5db67376df7d
proof step: reset goal_facts;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Mon Feb 14 12:23:08 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Feb 14 20:42:02 2000 +0100
     1.3 @@ -496,6 +496,7 @@
     1.4    state
     1.5    |> Proof.assert_backward
     1.6    |> refine (if_none opt_text default_text)
     1.7 +  |> Seq.map (Proof.goal_facts (K []))
     1.8    |> Seq.map Proof.enter_forward;
     1.9  
    1.10  fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));