src/HOL/Tools/function_package/fundef_datatype.ML

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 08 02:13:02 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 08 09:08:54 2006 +0100
@@ -192,7 +192,7 @@
     lthy
       |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
       ||> by_pat_completeness_simp
-      (*|-> termination_by_lexicographic_order*) |> snd
+      |-> termination_by_lexicographic_order
 
 
 val funP =