# HG changeset patch
# User wenzelm
# Date 1231180635 -3600
# Node ID aa8689d93135f224da51b31bbb1603282009ce8d
# Parent  642cac18e155add9a94bd6a1bf75632f865dc79d# Parent  59250869ced58342452499dbd84e15fc9c668bee
merged

diff -r 642cac18e155 -r aa8689d93135 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jan 05 18:13:26 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jan 05 19:37:15 2009 +0100
@@ -199,13 +199,13 @@
 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
 
 val by_pat_completeness_simp =
-    Proof.global_terminal_proof
+    Proof.future_terminal_proof
       (Method.Basic (pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.global_terminal_proof
+    #> Proof.future_terminal_proof
       (Method.Basic (method, Position.none), NONE)
 
 fun mk_catchall fixes arities =