# HG changeset patch
# User wenzelm
# Date 1136332365 -3600
# Node ID 15178f4aa2030ba39d26caafb1c99be6cef04345
# Parent  b0e13463747991f84a30c31b91f4ea542625c876
moved forget_proof to toplevel.ML;

diff -r b0e134637479 -r 15178f4aa203 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Jan 04 00:52:43 2006 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Jan 04 00:52:45 2006 +0100
@@ -43,7 +43,6 @@
   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
-  val forget_proof: Toplevel.transition -> Toplevel.transition
   val begin_theory: string -> string list -> (string * bool) list -> bool -> theory
   val end_theory: theory -> theory
   val kill_theory: string -> unit
@@ -157,10 +156,6 @@
 val done_proof = local_done_proof o global_done_proof;
 val skip_proof = local_skip_proof o global_skip_proof;
 
-val forget_proof =
-  Toplevel.proof_to_theory Proof.theory_of o
-  Toplevel.skip_proof_to_theory (K true);
-
 
 (* theory init and exit *)