src/Tools/case_product.ML
changeset 52732 b4da1f2ec73f
parent 48902 44a6967240b7
child 54742 7a86358a3c0b
--- 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 =