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.
tuned;
authorwenzelm
Wed, 08 Mar 2006 18:37:27 +0100
changeset 19221 aab0c0399e91
parent 19220 05b00acff957
child 19222 111ba44c66b2
tuned;
src/Pure/goal.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/goal.ML	Wed Mar 08 18:37:25 2006 +0100
+++ b/src/Pure/goal.ML	Wed Mar 08 18:37:27 2006 +0100
@@ -179,10 +179,10 @@
    else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
   |> Seq.map (Thm.adjust_maxidx #> init);
 
-fun retrofit i n st' =
-  (if n = 1 then I
-   else Drule.rotate_prems (i - 1) #> Drule.conj_uncurry n #> Drule.rotate_prems (1 - i))
-  #> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
+fun retrofit i n st' st =
+  (if n = 1 then st
+   else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
+  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
 
 fun SELECT_GOAL tac i st =
   if Thm.nprems_of st = 1 andalso i = 1 then tac st
isabelle