Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 15 Jul 2008 12:13:14 +0200
changeset 27603 69c00b56fb36
parent 27602 86cf8f2493ca
child 27604 6c347b96d941
tuned;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 15 11:50:04 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 15 12:13:14 2008 +0200
@@ -168,7 +168,7 @@
 
 (* current node *)
 
-fun previous_node_of (State (_, prev_node)) = Option.map #1 prev_node;
+fun previous_node_of (State (_, prev)) = Option.map #1 prev;
 
 fun node_of (State (NONE, _)) = raise UNDEF
   | node_of (State (SOME (node, _), _)) = node;
@@ -367,8 +367,8 @@
 
 fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
-  | apply_tr _ _ Exit (State (SOME (node as Theory (Context.Theory _, _), exit), _)) =
-      State (NONE, SOME (node, exit))
+  | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
+      State (NONE, prev)
   | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
       (controlled_execution exit thy; toplevel)
   | apply_tr int _ (Keep f) state =
isabelle