# HG changeset patch
# User wenzelm
# Date 949092997 -3600
# Node ID 97414b447a022501a0de07a28497d3f0bd3cf0d7
# Parent  651b006d7eb8897e24402e76d27f2e006e457a6d
added HEADGOAL;

diff -r 651b006d7eb8 -r 97414b447a02 src/Pure/Isar/proof.ML
--- 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;