--- a/src/Pure/tctical.ML Mon Nov 14 10:46:50 1994 +0100
+++ b/src/Pure/tctical.ML Mon Nov 14 10:49:39 1994 +0100
@@ -444,10 +444,9 @@
(*Does the work of SELECT_GOAL. *)
fun select (Tactic tf) state i =
- let val prem::_ = drop(i-1, prems_of state)
- val st0 = trivial (cterm_of (#sign(rep_thm state)) prem);
+ let val cprem::_ = drop(i-1, cprems_of state)
fun next st = bicompose false (false, st, nprems_of st) i state
- in Sequence.flats (Sequence.maps next (tf st0))
+ in Sequence.flats (Sequence.maps next (tf (trivial cprem)))
end;
fun SELECT_GOAL tac i = Tactic (fn state =>