src/HOL/Code_Generator.thy

--- a/src/HOL/Code_Generator.thy	Fri Nov 03 14:22:34 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Fri Nov 03 14:22:35 2006 +0100
@@ -116,7 +116,7 @@
 let
   fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
     (Drule.goals_conv (equal i) (HOL.Trueprop_conv
-      (HOL.Equals_conv NBE.normalization_conv))));
+      NBE.normalization_conv)));
   val normalization_meth =
     Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
 in