src/ZF/int_arith.ML

--- a/src/ZF/int_arith.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/ZF/int_arith.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -112,7 +112,7 @@
 
 (*push the unary minus down: - x * y = x * - y *)
 val int_minus_mult_eq_1_to_2 =
-    [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
+    [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> Drule.standard;
 
 (*to extract again any uncancelled minuses*)
 val int_minus_from_mult_simps =