--- a/src/Tools/case_product.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/case_product.ML Sat Jul 27 16:35:51 2013 +0200
@@ -70,10 +70,9 @@
val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
val thm2' = thm2 OF p_cons2
in
- Tactic.rtac (thm1 OF p_cons1)
+ rtac (thm1 OF p_cons1)
THEN' EVERY' (map (fn p =>
- Tactic.rtac thm2'
- THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
+ rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
end
fun combine ctxt thm1 thm2 =