# HG changeset patch # User wenzelm # Date 954961339 -7200 # Node ID d69616c7421179a04624e50350b33217ab9bde01 # Parent 3ccb29fb26ef76bb04967543f812705fd00c5b37 tuned comment; diff -r 3ccb29fb26ef -r d69616c74211 src/Pure/Isar/proof.ML --- 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;