changeset 30510 | 4120fc59dd85 |
parent 30493 | b8570ea1ce25 |
child 30515 | bca05b17b618 |
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 19:58:26 2009 +0100 @@ -203,7 +203,7 @@ handle COMPLETENESS => no_tac) -fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt) +fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt) val by_pat_completeness_auto = Proof.global_future_terminal_proof