# HG changeset patch
# User wenzelm
# Date 861295543 -7200
# Node ID 83a4c4f79dcd45e4e0eabc2a5f620c54c9162ba0
# Parent  6c035c126d7f9eef1617bd3bf5c74ab6b9101590
renamed set_ap to setmp;

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);