dropped equals_conv for nbe
authorhaftmann
Fri, 03 Nov 2006 14:22:35 +0100
changeset 21149 ee207b9b8bf5
parent 21148 3a64d58a9f49
child 21150 405ebd7ba881
dropped equals_conv for nbe
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