# HG changeset patch # User wenzelm # Date 1216067213 -7200 # Node ID 5e499b223a1e4b7fca8c2580481d0f540cd78f65 # Parent 26415966c7086b9615082863ae250b3b1275b61c tuned message; diff -r 26415966c708 -r 5e499b223a1e src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jul 14 22:09:08 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jul 14 22:26:53 2008 +0200 @@ -143,7 +143,7 @@ if ThyInfo.check_known_thy name then (Isar.commit_exit (); ThyInfo.touch_child_thys name; ThyInfo.register_thy name) handle ERROR msg => - (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); + (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); tell_file_retracted (ThyLoad.thy_path name)) else (); val _ = Isar.init_point ();