src/Pure/subgoal.ML
changeset 52223 5bb6ae8acb87
parent 49845 9b19c0e81166
child 54883 dd04a8b654fc
--- a/src/Pure/subgoal.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/subgoal.ML	Wed May 29 18:25:11 2013 +0200
@@ -125,7 +125,10 @@
       |> fold (Thm.forall_elim o #2) subgoal_inst
       |> Thm.adjust_maxidx_thm idx
       |> singleton (Variable.export ctxt2 ctxt0);
-  in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
+  in
+    Thm.bicompose {flatten = true, match = false, incremented = false}
+      (false, result, Thm.nprems_of st1) i st0
+  end;
 
 
 (* tacticals *)