# HG changeset patch
# User haftmann
# Date 1162560155 -3600
# Node ID ee207b9b8bf588c72784acd7937a27c5cd9aebb9
# Parent  3a64d58a9f492993cea183d9645af60c57271502
dropped equals_conv for nbe

diff -r 3a64d58a9f49 -r ee207b9b8bf5 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