# HG changeset patch
# User wenzelm
# Date 1126952284 -7200
# Node ID b94e2897776adfb7ef296b6542110c732a437d52
# Parent  3a23acfdf5ba9dc1b7a25b8ccda726f9fcc29b0d
theorem(_i): empty target;
forget_proof: removed tmp hack;

diff -r 3a23acfdf5ba -r b94e2897776a src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sat Sep 17 12:18:03 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat Sep 17 12:18:04 2005 +0200
@@ -105,7 +105,7 @@
   opt_chain #> goal (K (K Seq.single)) stmt int;
 
 fun global_goal goal kind a propp thy =
-  goal kind (K (K I)) NONE a [(("", []), [propp])] (ProofContext.init thy);
+  goal kind (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);
 
 in
 
@@ -160,8 +160,7 @@
 val skip_proof = local_skip_proof o global_skip_proof;
 
 val forget_proof =
-  Toplevel.proof_to_theory (Sign.local_path o Sign.restore_naming ProtoPure.thy o   (* FIXME tmp *)
-    Proof.theory_of o ProofHistory.current) o
+  Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current) o
   Toplevel.skip_proof_to_theory (K true);