src/HOL/Tools/numeral_simprocs.ML

--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -210,7 +210,7 @@
 
 (*push the unary minus down: - x * y = x * - y *)
 val minus_mult_eq_1_to_2 =
-    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
+    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> Drule.standard;
 
 (*to extract again any uncancelled minuses*)
 val minus_from_mult_simps =