Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
authorlcp
Mon, 14 Nov 1994 10:49:39 +0100
changeset 709 0d0df9b5afe3
parent 708 8422e50adce0
child 710 53fef17a729a
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of: new SELECT_GOAL is MUCH faster
src/Pure/tctical.ML file | annotate | diff | comparison | revisions 
--- 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 =>
isabelle