removed set quick_and_dirty and ThmDeps.enable -- no effect here;
authorwenzelm
Fri Feb 10 02:22:29 2006 +0100 (2006-02-10)
changeset 18993f055b4fe381e
parent 18992 910fbe64033c
child 18994 ce724d5bada2
removed set quick_and_dirty and ThmDeps.enable -- no effect here;
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Feb 10 02:22:24 2006 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Fri Feb 10 02:22:29 2006 +0100
     1.3 @@ -1426,13 +1426,11 @@
     1.4      set initialized; ()));
     1.5    sync_thy_loader ();
     1.6    change print_mode (cons proof_generalN o remove (op =) proof_generalN);
     1.7 -  init_pgip_session_id();
     1.8 +  init_pgip_session_id ();
     1.9    if pgip then
    1.10 -      (change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
    1.11 +    change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN])
    1.12    else
    1.13      pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
    1.14 -  set quick_and_dirty;
    1.15 -  ThmDeps.enable ();
    1.16    set_prompts isar pgip;
    1.17    pgip_active := pgip);
    1.18