diff -r d24b2692562f -r 198eae6f5a35 src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Thu May 28 22:53:23 2009 -0700 +++ b/src/HOL/Library/normarith.ML Thu May 28 22:54:57 2009 -0700 @@ -391,7 +391,7 @@ fun init_conv ctxt = Simplifier.rewrite (Simplifier.context ctxt - (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) + (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_vector_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) then_conv field_comp_conv then_conv nnf_conv