removed set quick_and_dirty and ThmDeps.enable -- no effect here;
authorwenzelm
Fri, 10 Feb 2006 02:22:29 +0100
changeset 18993 f055b4fe381e
parent 18992 910fbe64033c
child 18994 ce724d5bada2
removed set quick_and_dirty and ThmDeps.enable -- no effect here;
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);