author | wenzelm |
Thu, 18 Jan 2001 21:41:36 +0100 | |
changeset 10938 | 2c85f2416c1b |
parent 10937 | 5651e0636e38 |
child 10939 | fe14e54594a3 |
--- a/src/Pure/Isar/proof.ML Thu Jan 18 20:40:47 2001 +0100 +++ b/src/Pure/Isar/proof.ML Thu Jan 18 21:41:36 2001 +0100 @@ -619,7 +619,8 @@ (*local goals*) -fun local_goal' prepp kind check f name atts args int state = +fun local_goal' prepp kind (check: bool -> state -> state) + f name atts args int state = state |> setup_goal open_block prepp kind f name atts args |> warn_extra_tfrees state