# HG changeset patch
# User paulson
# Date 841940983 -7200
# Node ID 5309416236b6a06edfdb1a3300e5e8d487f8504d
# Parent  4b5b2d04782ce42532100e8d85a0d6c4b5f7b17f
Added thin_tac to signature; previous change was useless

diff -r 4b5b2d04782c -r 5309416236b6 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Sep 05 18:28:54 1996 +0200
+++ b/src/Pure/tactic.ML	Thu Sep 05 18:29:43 1996 +0200
@@ -77,6 +77,7 @@
   val subgoal_tac: string -> int -> tactic
   val subgoals_tac: string list -> int -> tactic
   val subgoals_of_brl: bool * thm -> int
+  val thin_tac: string -> int -> tactic
   val trace_goalno_tac: (int -> tactic) -> int -> tactic
   end;