# HG changeset patch
# User wenzelm
# Date 1552173832 -3600
# Node ID 6db51f45b5f93c5e6c6cf7f0968843647def75ed
# Parent  b9985133805d117899bc26e2358121e2a8128506
tuned;

diff -r b9985133805d -r 6db51f45b5f9 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:21:34 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Mar 10 00:23:52 2019 +0100
@@ -252,11 +252,23 @@
 
 (** toplevel transitions **)
 
-(* node transactions -- maintaining stable checkpoints *)
+(* primitive transitions *)
+
+datatype trans =
+  (*init theory*)
+  Init of unit -> theory |
+  (*formal exit of theory*)
+  Exit |
+  (*peek at state*)
+  Keep of bool -> state -> unit |
+  (*node transaction and presentation*)
+  Transaction of (bool -> node -> node_presentation) * (state -> unit);
+
+local
 
 exception FAILURE of state * exn;
 
-fun apply_transaction f g node =
+fun apply f g node =
   let
     val node_pr = node_presentation node;
     val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
@@ -273,21 +285,6 @@
     | SOME exn => raise FAILURE (result, exn))
   end;
 
-
-(* primitive transitions *)
-
-datatype trans =
-  (*init theory*)
-  Init of unit -> theory |
-  (*formal exit of theory*)
-  Exit |
-  (*peek at state*)
-  Keep of bool -> state -> unit |
-  (*node transaction and presentation*)
-  Transaction of (bool -> node -> node_presentation) * (state -> unit);
-
-local
-
 fun apply_tr int trans state =
   (case (trans, node_of state) of
     (Init f, Toplevel) =>
@@ -296,7 +293,7 @@
   | (Exit, node as Theory (Context.Theory thy)) =>
       let
         val State ((node', pr_ctxt), _) =
-          node |> apply_transaction
+          node |> apply
             (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
             (K ());
       in State ((Toplevel, pr_ctxt), get_theory node') end
@@ -304,7 +301,7 @@
       Runtime.controlled_execution (try generic_theory_of state)
         (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
   | (Transaction _, Toplevel) => raise UNDEF
-  | (Transaction (f, g), node) => apply_transaction (fn x => f int x) g node
+  | (Transaction (f, g), node) => apply (fn x => f int x) g node
   | _ => raise UNDEF);
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)