--- a/src/Pure/Isar/proof.ML Fri Jan 28 21:56:02 2000 +0100
+++ b/src/Pure/Isar/proof.ML Fri Jan 28 21:56:37 2000 +0100
@@ -8,6 +8,7 @@
signature BASIC_PROOF =
sig
val FINDGOAL: (int -> tactic) -> tactic
+ val HEADGOAL: (int -> tactic) -> tactic
end;
signature PROOF =
@@ -418,6 +419,8 @@
let fun find (i, n) = if i > n then no_tac else tac i APPEND find (i + 1, n)
in find (1, nprems_of st) st end;
+fun HEADGOAL tac = tac 1;
+
fun export_goal print_rule raw_rule inner state =
let
val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state;