Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/fundef_datatype.ML
changeset 23056 448827ccd9e9
parent 22899 5ea718c68123
child 23189 4574ab8f3b21 
--- 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,
isabelle