src/Tools/case_product.ML
changeset 52732 b4da1f2ec73f
parent 48902 44a6967240b7
child 54742 7a86358a3c0b
     1.1 --- a/src/Tools/case_product.ML	Thu Jul 25 16:46:53 2013 +0200
     1.2 +++ b/src/Tools/case_product.ML	Sat Jul 27 16:35:51 2013 +0200
     1.3 @@ -70,10 +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 -    Tactic.rtac (thm1 OF p_cons1)
     1.8 +    rtac (thm1 OF p_cons1)
     1.9       THEN' EVERY' (map (fn p =>
    1.10 -       Tactic.rtac thm2'
    1.11 -       THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
    1.12 +       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
    1.13    end
    1.14  
    1.15  fun combine ctxt thm1 thm2 =