src/Pure/subgoal.ML
changeset 52223 5bb6ae8acb87
parent 49845 9b19c0e81166
child 54883 dd04a8b654fc
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   123       |> Drule.implies_intr_list subgoals
   123       |> Drule.implies_intr_list subgoals
   124       |> fold_rev (Thm.forall_intr o #1) subgoal_inst
   124       |> fold_rev (Thm.forall_intr o #1) subgoal_inst
   125       |> fold (Thm.forall_elim o #2) subgoal_inst
   125       |> fold (Thm.forall_elim o #2) subgoal_inst
   126       |> Thm.adjust_maxidx_thm idx
   126       |> Thm.adjust_maxidx_thm idx
   127       |> singleton (Variable.export ctxt2 ctxt0);
   127       |> singleton (Variable.export ctxt2 ctxt0);
   128   in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
   128   in
       
   129     Thm.bicompose {flatten = true, match = false, incremented = false}
       
   130       (false, result, Thm.nprems_of st1) i st0
       
   131   end;
   129 
   132 
   130 
   133 
   131 (* tacticals *)
   134 (* tacticals *)
   132 
   135 
   133 fun GEN_FOCUS flags tac ctxt i st =
   136 fun GEN_FOCUS flags tac ctxt i st =