# HG changeset patch
# User wenzelm
# Date 1006986588 -3600
# Node ID edeb1bbcd4797f6a9e53b1cbc8fbd78a2f4c5627
# Parent  160013745a9287cf815012fe195601ad1c7633e8
added proof_to_theory';

diff -r 160013745a92 -r edeb1bbcd479 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Nov 28 23:29:21 2001 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Nov 28 23:29:48 2001 +0100
@@ -53,6 +53,7 @@
   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
+  val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
@@ -348,7 +349,9 @@
   app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
 val proof = proof' o K;
-fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
+fun proof_to_theory' f =
+  map_current (fn int => (fn Proof prf => Theory (f int prf) | _ => raise UNDEF));
+val proof_to_theory = proof_to_theory' o K;
 
 val unknown_theory = imperative (fn () => warning "Unknown theory context");
 val unknown_proof = imperative (fn () => warning "Unknown proof context");