--- a/src/HOL/Tools/Function/pat_completeness.ML Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML Thu Apr 12 18:39:19 2012 +0200
@@ -7,11 +7,8 @@
signature PAT_COMPLETENESS =
sig
val pat_completeness_tac: Proof.context -> int -> tactic
- val pat_completeness: Proof.context -> Proof.method
val prove_completeness : theory -> term list -> term -> term list list ->
term list list -> thm
-
- val setup : theory -> theory
end
structure Pat_Completeness : PAT_COMPLETENESS =
@@ -153,11 +150,4 @@
end
handle COMPLETENESS => no_tac)
-
-val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
-
-val setup =
- Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
- "Completeness prover for datatype patterns"
-
end