# HG changeset patch
# User chaieb
# Date 1234198630 0
# Node ID 4bb780545478e2d074b83aeb263243ea28b91442
# Parent  4ac60c7d9b786ede66cc1167cd9f57d4e6a5e5c7
Fixed theorem reference

diff -r 4ac60c7d9b78 -r 4bb780545478 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Mon Feb 09 16:54:03 2009 +0000
+++ b/src/HOL/Library/normarith.ML	Mon Feb 09 16:57:10 2009 +0000
@@ -1043,7 +1043,7 @@
   then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq;
 
 local
- val pth_zero = @{thm "Vectors.norm_0"}
+ val pth_zero = @{thm "norm_0"}
  val tv_n = (hd o tl o dest_ctyp o ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of)
              pth_zero
  val concl = dest_arg o cprop_of