--- 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 |>