# HG changeset patch
# User berghofe
# Date 1188317061 -7200
# Node ID 86cf57ddf8f67ac9ab6baf6319ce1a5d72270579
# Parent  93b113c5ac332e41e60fd47cacf6f64e085763ef
Added local_theory_to_proof'

diff -r 93b113c5ac33 -r 86cf57ddf8f6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Aug 28 18:03:16 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Aug 28 18:04:21 2007 +0200
@@ -71,6 +71,8 @@
   val end_local_theory: transition -> transition
   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
   val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
+  val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
+    transition -> transition
   val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
     transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
@@ -580,7 +582,7 @@
 fun begin_proof init finish = app_current (fn int =>
   (fn Theory (gthy, _) =>
     let
-      val prf = init gthy;
+      val prf = init int gthy;
       val schematic = Proof.schematic_goal prf;
     in
       if ! skip_proofs andalso schematic then
@@ -595,10 +597,11 @@
 
 in
 
-fun local_theory_to_proof loc f = begin_proof (f o loc_begin loc) (loc_finish loc);
+fun local_theory_to_proof' loc f = begin_proof (fn int => f int o loc_begin loc) (loc_finish loc);
+fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
 
 fun theory_to_proof f = begin_proof
-    (fn Context.Theory thy => f thy | _ => raise UNDEF)
+    (K (fn Context.Theory thy => f thy | _ => raise UNDEF))
     (K (Context.Theory o ProofContext.theory_of));
 
 end;