# 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