diff -r 6c035c126d7f -r 83a4c4f79dcd src/Pure/library.ML
--- 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);