| changeset 2978 | 83a4c4f79dcd |
| parent 2958 | 7837471d2f27 |
| child 3063 | 963e3bf01799 |
--- a/src/Pure/library.ML Thu Apr 17 18:17:23 1997 +0200 +++ b/src/Pure/library.ML Thu Apr 17 18:45:43 1997 +0200 @@ -142,7 +142,7 @@ fun reset flag = (flag := false; false); fun toggle flag = (flag := not (! flag); ! flag); -fun set_ap flag value f x = +fun setmp flag value f x = let val orig_value = ! flag; fun return y = (flag := orig_value; y);