# HG changeset patch
# User wenzelm
# Date 1139534549 -3600
# Node ID f055b4fe381e4bc38e7436bc784db87d1ac0d4ae
# Parent  910fbe64033c3e4ad148ec8d04a6655fbdbb9855
removed set quick_and_dirty and ThmDeps.enable -- no effect here;

diff -r 910fbe64033c -r f055b4fe381e src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Feb 10 02:22:24 2006 +0100
+++ b/src/Pure/proof_general.ML	Fri Feb 10 02:22:29 2006 +0100
@@ -1426,13 +1426,11 @@
     set initialized; ()));
   sync_thy_loader ();
   change print_mode (cons proof_generalN o remove (op =) proof_generalN);
-  init_pgip_session_id();
+  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 fold (remove (op =)) [pgmlN, pgmlatomsN])
   else
     pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
-  set quick_and_dirty;
-  ThmDeps.enable ();
   set_prompts isar pgip;
   pgip_active := pgip);