next_block: allow in non-goal blocks as well (experimental);
authorwenzelm
Fri Mar 17 16:26:43 2000 +0100 (2000-03-17)
changeset 849421074180a6f2
parent 8493 60c2f892b1d9
child 8495 4f5a3272c8ba
next_block: allow in non-goal blocks as well (experimental);
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Mar 17 15:51:13 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 17 16:26:43 2000 +0100
     1.3 @@ -748,7 +748,7 @@
     1.4    state
     1.5    |> assert_forward
     1.6    |> close_block
     1.7 -  |> assert_current_goal true
     1.8 +(*  |> assert_current_goal true  *)  (* FIXME !? *)
     1.9    |> new_block;
    1.10  
    1.11