--- a/src/Pure/Isar/proof.ML Wed Apr 05 21:01:59 2000 +0200 +++ b/src/Pure/Isar/proof.ML Wed Apr 05 21:02:19 2000 +0200 @@ -703,7 +703,6 @@ state |> assert_forward |> close_block -(* |> assert_current_goal true *) (* FIXME !? *) |> new_block;