# HG changeset patch
# User lcp
# Date 784806579 -3600
# Node ID 0d0df9b5afe34bee9f2da4cf63f9a96d73dc4117
# Parent  8422e50adce0519d3eb28aec842fd6c5d2bb0359
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
new SELECT_GOAL is MUCH faster

diff -r 8422e50adce0 -r 0d0df9b5afe3 src/Pure/tctical.ML
--- 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 =>