changeset 58950 | d07464875dd4 |
parent 58009 | 987c848d509b |
child 60372 | b62eaac5c1af |
--- a/src/Pure/par_tactical.ML Sat Nov 08 17:39:01 2014 +0100 +++ b/src/Pure/par_tactical.ML Sat Nov 08 21:31:51 2014 +0100 @@ -35,7 +35,7 @@ fun retrofit st' = rotate_prems ~1 #> - Thm.bicompose {flatten = false, match = false, incremented = false} + Thm.bicompose NONE {flatten = false, match = false, incremented = false} (false, Goal.conclude st', Thm.nprems_of st') 1; in