src/Pure/par_tactical.ML
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