# HG changeset patch
# User krauss
# Date 1179758398 -7200
# Node ID 448827ccd9e9adafe6ec81f341b5cd426275d24a
# Parent  34158639dc128e97b89f1f198d985be16258c9c4
fixed signature

diff -r 34158639dc12 -r 448827ccd9e9 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon May 21 16:22:46 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon May 21 16:39:58 2007 +0200
@@ -170,7 +170,7 @@
 
 val termination_by_lexicographic_order =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE)
+    #> Proof.global_terminal_proof (Method.Basic (LexicographicOrder.lexicographic_order []), NONE)
 
 val setup =
     Method.add_methods [("pat_completeness", Method.no_args pat_completeness,
diff -r 34158639dc12 -r 448827ccd9e9 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 21 16:22:46 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 21 16:39:58 2007 +0200
@@ -7,7 +7,7 @@
 
 signature LEXICOGRAPHIC_ORDER =
 sig
-  val lexicographic_order : Proof.context -> Method.method
+  val lexicographic_order : thm list -> Proof.context -> Method.method
 
   (* exported for use by size-change termination prototype.
      FIXME: provide a common interface later *)