# HG changeset patch
# User nipkow
# Date 1151684782 -7200
# Node ID d6e238c46d1b0761e25c60d399b084dcb40e165b
# Parent  c72e2110c026cbb907191cb9fce1efcf1fe7a53d
normalization uses refl now

diff -r c72e2110c026 -r d6e238c46d1b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jun 30 12:22:29 2006 +0200
+++ b/src/HOL/HOL.thy	Fri Jun 30 18:26:22 2006 +0200
@@ -1290,7 +1290,7 @@
   (Drule.goals_conv (equal i) normalization_conv));
 
 val normalization_meth =
-  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN rtac TrueI 1));
+  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI,refl] 1));
 
 in