src/Tools/case_product.ML
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 59498 50b60f501b05
     1.1 --- a/src/Tools/case_product.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Tools/case_product.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -70,9 +70,9 @@
     1.4      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
     1.5      val thm2' = thm2 OF p_cons2
     1.6    in
     1.7 -    rtac (thm1 OF p_cons1)
     1.8 +    resolve_tac [thm1 OF p_cons1]
     1.9       THEN' EVERY' (map (fn p =>
    1.10 -       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
    1.11 +       resolve_tac [thm2'] THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
    1.12    end
    1.13  
    1.14  fun combine ctxt thm1 thm2 =