--- a/src/Tools/misc_legacy.ML Wed May 29 16:12:05 2013 +0200
+++ b/src/Tools/misc_legacy.ML Wed May 29 18:25:11 2013 +0200
@@ -203,7 +203,9 @@
(forall_intr_list cparams (implies_intr_list chyps Cth)))
end
(*function to replace the current subgoal*)
- fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
+ fun next st =
+ Thm.bicompose {flatten = true, match = false, incremented = false}
+ (false, relift st, nprems_of st) gno state
in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
fun print_vars_terms n thm =