1.1 --- a/src/Pure/Interface/proof_general.ML	Wed Oct 20 15:50:51 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Wed Oct 20 15:53:22 1999 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4  
     1.5  fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
     1.6  
     1.7 -fun isa_action action name =
     1.8 +fun trace_action action name =
     1.9    let
    1.10      val update = (action = ThyInfo.Update);
    1.11      fun loaded ((path, _), really) =
    1.12 @@ -155,12 +155,8 @@
    1.13      else seq (tell_pg "you can unlock the file") files
    1.14    end;
    1.15  
    1.16 -fun isar_action action name =
    1.17 -  if action = ThyInfo.Update then tell_pg "this theory is loaded:" name
    1.18 -  else tell_pg "you can unlock the theory" name;
    1.19 -
    1.20  in
    1.21 -  fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action);
    1.22 +  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
    1.23  end;
    1.24  
    1.25  
    1.26 @@ -190,7 +186,7 @@
    1.27  fun init isar =
    1.28   (setup_messages ();
    1.29    setup_state isar;
    1.30 -  setup_thy_loader isar;
    1.31 +  setup_thy_loader ();
    1.32    print_mode := [proof_generalN];
    1.33    set quick_and_dirty;
    1.34    if isar then Isar.sync_main () else isa_restart ());