--- 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,
--- 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 *)