diff -r ac2732072403 -r 1bbb31aaf98d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Oct 12 22:57:42 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Oct 12 22:57:45 2006 +0200
@@ -28,7 +28,7 @@
   val theory_of: state -> theory
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
-  val enter_forward_proof: state -> Proof.state
+  val enter_proof_body: state -> Proof.state
   val prompt_state_default: state -> string
   val prompt_state_fn: (state -> string) ref
   val print_state_context: state -> unit
@@ -70,25 +70,27 @@
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
-  val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
-    -> transition -> transition
+  val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
+    transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
-  val exit_local_theory: transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
+  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 -> (local_theory -> Proof.state) ->
+    transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
+  val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
+  val forget_proof: transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
+  val present_proof: (bool -> node -> unit) -> transition -> transition
   val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val skip_proof: (int History.T -> int History.T) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
-  val forget_proof: transition -> transition
-  val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
-  val present_proof: (bool -> node -> unit) -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
@@ -118,8 +120,9 @@
 
 datatype node =
   Theory of generic_theory * Proof.context option | (*theory with presentation context*)
-  Proof of ProofHistory.T * generic_theory |        (*history of proof states, original theory*)
-  SkipProof of (int History.T * generic_theory) * generic_theory;
+  Proof of ProofHistory.T * ((Proof.context -> generic_theory) * generic_theory) |
+    (*history of proof states, finish, original theory*)
+  SkipProof of int History.T * (generic_theory * generic_theory);
     (*history of proof depths, resulting theory, original theory*)
 
 val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
@@ -127,7 +130,7 @@
 
 fun cases_node f _ (Theory (gthy, _)) = f gthy
   | cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf)
-  | cases_node f _ (SkipProof ((_, gthy), _)) = f gthy;
+  | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
 
 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
   | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
@@ -148,7 +151,7 @@
         Theory (Context.Theory _, _) => 0
       | Theory (Context.Proof _, _) => 1
       | Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1
-      | SkipProof ((h, _), _) => History.current h + 2);   (*different notion of proof depth!*)
+      | SkipProof (h, _) => History.current h + 2);   (*different notion of proof depth!*)
 
 fun str_of_state (State NONE) = "at top level"
   | str_of_state (State (SOME (node, _))) =
@@ -183,7 +186,7 @@
     Proof (prf, _) => ProofHistory.position prf
   | _ => raise UNDEF);
 
-val enter_forward_proof = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
+val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
 
 
 (* prompt state *)
@@ -205,7 +208,7 @@
 fun pretty_node prf_only (Theory (gthy, _)) = if prf_only then [] else pretty_context gthy
   | pretty_node _ (Proof (prf, _)) =
       Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
-  | pretty_node _ (SkipProof ((h, _), _)) =
+  | pretty_node _ (SkipProof (h, _)) =
       [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))];
 
 fun pretty_state prf_only state =
@@ -497,7 +500,7 @@
 val print3 = print' three_buffersN;
 
 
-(* build transitions *)
+(* basic transitions *)
 
 val reset = add_trans Reset;
 fun init f exit kill = add_trans (Init (f, (exit, kill)));
@@ -516,8 +519,12 @@
     (fn Theory (Context.Theory thy, _) => exit thy | _ => raise UNDEF)
     (fn Theory (Context.Theory thy, _) => kill thy | _ => raise UNDEF);
 
+val unknown_theory = imperative (fn () => warning "Unknown theory context");
+val unknown_proof = imperative (fn () => warning "Unknown proof context");
+val unknown_context = imperative (fn () => warning "Unknown context");
 
-(* typed transitions *)
+
+(* theory transitions *)
 
 fun theory' f = app_current (fn int =>
   (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
@@ -525,12 +532,6 @@
 
 fun theory f = theory' (K f);
 
-val exit_local_theory = app_current (fn int =>
-  (fn Theory (Context.Proof lthy, _) =>
-      let val (ctxt', thy') = LocalTheory.exit int lthy
-      in Theory (Context.Theory thy', SOME ctxt') end
-    | _ => raise UNDEF));
-
 fun begin_local_theory begin f = app_current (fn int =>
   (fn Theory (Context.Theory thy, _) =>
         let
@@ -541,6 +542,14 @@
         in Theory (gthy, SOME ctxt) end
     | _ => raise UNDEF));
 
+val end_local_theory = app_current (fn int =>
+  (fn Theory (Context.Proof lthy, _) =>
+      let val (ctxt', thy') = LocalTheory.exit int lthy
+      in Theory (Context.Theory thy', SOME ctxt') end
+    | _ => raise UNDEF));
+
+local
+
 fun local_theory_presentation loc f g = app_current (fn int =>
   (fn Theory (Context.Theory thy, _) =>
         let val (ctxt', thy') = TheoryTarget.mapping loc f thy
@@ -552,77 +561,103 @@
         in Theory (Context.Proof lthy', SOME ctxt') end
     | _ => raise UNDEF) #> tap (g int));
 
+in
+
 fun local_theory loc f = local_theory_presentation loc f (K I);
 fun present_local_theory loc g = local_theory_presentation loc I g;
 
-fun theory_to_proof f = app_current (fn int =>
-  (fn Theory (gthy as Context.Theory thy, _) =>
-    let
-      val prf = f thy;
+end;
+
+
+(* proof transitions *)
+
+local
+
+fun begin_proof init finish = app_current (fn int =>
+  (fn Theory (gthy, _) =>
+    let 
+      val prf = init gthy;
       val schematic = Proof.schematic_goal prf;
     in
       if ! skip_proofs andalso schematic then
         warning "Cannot skip proof of schematic goal statement"
       else ();
       if ! skip_proofs andalso not schematic then
-        SkipProof ((History.init (undo_limit int) 0,
-          Context.Theory (ProofContext.theory_of (Proof.global_skip_proof int prf))), gthy)
-      else Proof (ProofHistory.init (undo_limit int) prf, gthy)
+        SkipProof
+          (History.init (undo_limit int) 0, (finish gthy (Proof.global_skip_proof int prf), gthy))
+      else Proof (ProofHistory.init (undo_limit int) prf, (finish gthy, gthy))
     end
   | _ => raise UNDEF));
 
+val global_finish = Context.Theory o ProofContext.theory_of;
+val local_finish = Context.Proof o LocalTheory.reinit;
+
+fun mixed_finish (Context.Theory _) ctxt = global_finish ctxt
+  | mixed_finish (Context.Proof lthy) ctxt =
+      Context.Proof (LocalTheory.raw_theory (K (ProofContext.theory_of ctxt)) lthy);
+
+in
+
+fun local_theory_to_proof NONE f = begin_proof
+      (fn Context.Theory thy => f (TheoryTarget.init NONE thy)
+        | Context.Proof lthy => f lthy)
+      (fn Context.Theory _ => global_finish
+        | Context.Proof _ => local_finish)
+  | local_theory_to_proof loc f =
+      begin_proof (f o TheoryTarget.init loc o Context.theory_of) mixed_finish;
+
+fun theory_to_proof f =
+  begin_proof (fn Context.Theory thy => f thy | _ => raise UNDEF) (K global_finish);
+
+end;
+
+fun end_proof f = map_current (fn int =>
+  (fn Proof (prf, (finish, orig_gthy)) =>
+        let val state = ProofHistory.current prf in
+          if can (Proof.assert_bottom true) state then
+            let
+              val ctxt' = f int state;
+              val gthy' = finish ctxt';
+            in Theory (gthy', SOME ctxt') end
+          else raise UNDEF
+        end
+    | SkipProof (h, (gthy, _)) =>
+        if History.current h = 0 then Theory (gthy, NONE) else raise UNDEF
+    | _ => raise UNDEF));
+
+val forget_proof = map_current (fn _ =>
+  (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
+    | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
+    | _ => raise UNDEF));
+
 fun proofs' f = map_current (fn int =>
-  (fn Proof (prf, orig_gthy) => Proof (ProofHistory.applys (f int) prf, orig_gthy)
-    | SkipProof ((h, gthy), orig_gthy) => SkipProof ((History.apply I h, gthy), orig_gthy)
+  (fn Proof (prf, x) => Proof (ProofHistory.applys (f int) prf, x)
+    | SkipProof (h, x) => SkipProof (History.apply I h, x)
     | _ => raise UNDEF));
 
 fun proof' f = proofs' (Seq.single oo f);
 val proofs = proofs' o K;
 val proof = proof' o K;
 
+fun present_proof f = map_current (fn int =>
+  (fn node as Proof _ => node
+    | node as SkipProof _ => node
+    | _ => raise UNDEF) #> tap (f int));
+
 fun actual_proof f = map_current (fn _ =>
-  (fn Proof (prf, orig_gthy) => Proof (f prf, orig_gthy)
+  (fn Proof (prf, x) => Proof (f prf, x)
     | _ => raise UNDEF));
 
 fun skip_proof f = map_current (fn _ =>
-  (fn SkipProof ((h, gthy), orig_gthy) => SkipProof ((f h, gthy), orig_gthy)
+  (fn SkipProof (h, x) => SkipProof (f h, x)
     | _ => raise UNDEF));
 
 fun skip_proof_to_theory p = map_current (fn _ =>
-  (fn SkipProof ((h, thy), _) =>
-    if p (History.current h) then Theory (thy, NONE)
+  (fn SkipProof (h, (gthy, _)) =>
+    if p (History.current h) then Theory (gthy, NONE)
     else raise UNDEF
   | _ => raise UNDEF));
 
-val forget_proof = map_current (fn _ =>
-  (fn Proof (_, orig_gthy) => Theory (orig_gthy, NONE)
-    | SkipProof (_, orig_gthy) => Theory (orig_gthy, NONE)
-    | _ => raise UNDEF));
-
-fun end_proof f = map_current (fn int =>
-  (fn Proof (prf, orig_gthy) =>
-        let val state = ProofHistory.current prf in
-          if can (Proof.assert_bottom true) state then
-            let
-              val ctxt' = f int state;
-              val gthy' =
-                if can Context.the_theory orig_gthy
-                then Context.Theory (ProofContext.theory_of ctxt')
-                else Context.Proof (LocalTheory.reinit ctxt');
-            in Theory (gthy', SOME ctxt') end
-          else raise UNDEF
-        end
-    | SkipProof ((h, gthy), _) =>
-        if History.current h = 0 then Theory (gthy, NONE) else raise UNDEF
-    | _ => raise UNDEF));
-
-fun present_proof f = map_current (fn int =>
-  (fn node as Proof _ => node | _ => raise UNDEF) #> tap (f int));
-
-val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_proof = imperative (fn () => warning "Unknown proof context");
-val unknown_context = imperative (fn () => warning "Unknown context");
-
 
 
 (** toplevel transactions **)