diff -r e4dc583a2d79 -r 3813cc8fad55 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Sep 15 13:35:21 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Sep 15 13:36:10 2005 +0200
@@ -160,7 +160,8 @@
 val skip_proof = local_skip_proof o global_skip_proof;
 
 val forget_proof =
-  Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current) o
+  Toplevel.proof_to_theory (Sign.local_path o Sign.restore_naming ProtoPure.thy o   (* FIXME tmp *)
+    Proof.theory_of o ProofHistory.current) o
   Toplevel.skip_proof_to_theory (K true);