diff -r 5f0610aafc48 -r 7689f81f8996 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/proof_general.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -1428,7 +1428,7 @@
   change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   init_pgip_session_id ();
   if pgip then
-    change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN])
+    change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN])
   else
     pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
   set_prompts isar pgip;