src/Tools/case_product.ML

--- a/src/Tools/case_product.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/Tools/case_product.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -74,7 +74,7 @@
     (Tactic.rtac (thm1 OF p_cons1)
      THEN' EVERY' (map (fn p =>
        Tactic.rtac thm2'
-       THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss)
+       THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
     )
   end