# HG changeset patch
# User wenzelm
# Date 1126784170 -7200
# Node ID 3813cc8fad5550c8dd548ed3e76c2a89282e0311
# Parent  e4dc583a2d797ecc9c78234b4897dd7ec80c7d4e
forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;

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);