--- a/src/Pure/Isar/toplevel.ML Fri Mar 16 13:05:30 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Mar 16 14:42:11 2012 +0100
@@ -90,8 +90,8 @@
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command: transition -> state -> state
- val excursion:
- (transition * transition list) list -> (transition * state) list future list * theory
+ val proof_result: bool -> transition * transition list -> state ->
+ (transition * state) list future * state
end;
structure Toplevel: TOPLEVEL =
@@ -644,7 +644,7 @@
in (st', st') end;
-(* excursion of units, consisting of commands with proof *)
+(* scheduled proof result *)
structure States = Proof_Data
(
@@ -692,12 +692,4 @@
in (result, st'') end
end;
-fun excursion input =
- let
- val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
- val immediate = not (Goal.future_enabled ());
- val (results, end_state) = fold_map (proof_result immediate) input toplevel;
- val thy = end_theory end_pos end_state;
- in (results, thy) end;
-
end;