# HG changeset patch
# User krauss
# Date 1166018047 -3600
# Node ID 453fd9857b4c36e0cc63c5e87ac38df042720d9b
# Parent  0fba71f35a9c00de15e6079638417ba22bd54e57
nat type now has a size functin => no longer needed as special case

diff -r 0fba71f35a9c -r 453fd9857b4c src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 13 14:52:50 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 13 14:54:07 2006 +0100
@@ -62,9 +62,7 @@
     | _ => [(t, tt)]
            
 fun mk_base_fun_header fulltyp (t, typ) =
-    if typ = HOLogic.natT then
-      Abs ("x", fulltyp, t)
-    else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
+    Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
          
 fun mk_base_funs (tt: typ) = 
     mk_base_fun_bodys (Bound 0) tt |>