| changeset 8242 | ac8ac0eba738 |
| parent 8240 | 87e08624e209 |
| child 8282 | 58a33fd5b30c |
--- a/src/Pure/Isar/method.ML Mon Feb 14 12:23:08 2000 +0100 +++ b/src/Pure/Isar/method.ML Mon Feb 14 20:42:02 2000 +0100 @@ -496,6 +496,7 @@ state |> Proof.assert_backward |> refine (if_none opt_text default_text) + |> Seq.map (Proof.goal_facts (K [])) |> Seq.map Proof.enter_forward; fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));