--- a/src/HOL/Tools/Function/fundef_datatype.ML Sat Jul 25 18:02:43 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML Sat Jul 25 18:04:15 2009 +0200
@@ -208,13 +208,12 @@
val by_pat_completeness_auto =
Proof.global_future_terminal_proof
- (Method.Basic (pat_completeness, Position.none),
+ (Method.Basic pat_completeness,
SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
fun termination_by method int =
Fundef.termination_proof NONE
- #> Proof.global_future_terminal_proof
- (Method.Basic (method, Position.none), NONE) int
+ #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
fun mk_catchall fixes arity_of =
let