src/HOL/Tools/function_package/lexicographic_order.ML

--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Apr 25 15:30:33 2008 +0200
@@ -50,7 +50,7 @@
         val mlexT = (domT --> HOLogic.natT) --> relT --> relT
         fun mk_ms [] = Const (@{const_name "{}"}, relT)
           | mk_ms (f::fs) = 
-            Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs
+            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
     in
         mk_ms mfuns
     end