# HG changeset patch # User wenzelm # Date 1231162166 -3600 # Node ID 59250869ced58342452499dbd84e15fc9c668bee # Parent c7735554d291c185f7f10c406ef07705dfe744cc parallelize some internal proofs via Proof.future_terminal_proof; diff -r c7735554d291 -r 59250869ced5 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jan 05 14:22:40 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jan 05 14:29:26 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 =