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