Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof.global_future_terminal_proof;
authorwenzelm
Wed, 07 Jan 2009 20:27:55 +0100
changeset 29387 d23fdfa46b6a
parent 29386 d5849935560c
child 29388 79eb3649ca9e
child 29394 4638ab6c878f
Proof.global_future_terminal_proof;
src/HOL/Tools/function_package/fundef_datatype.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Jan 07 20:27:23 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Jan 07 20:27:55 2009 +0100
@@ -199,13 +199,13 @@
 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
 
 val by_pat_completeness_simp =
-    Proof.future_terminal_proof
+    Proof.global_future_terminal_proof
       (Method.Basic (pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method int =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.future_terminal_proof
+    #> Proof.global_future_terminal_proof
       (Method.Basic (method, Position.none), NONE) int
 
 fun mk_catchall fixes arities =
isabelle