src/Pure/proof_general.ML

     setup_thy_loader ();
     setup_present_hook ();
     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);
 
 fun init isar =
  (init_setup isar false;