disable coercions for NO_MATCH
authorhoelzl
Thu, 30 Oct 2014 09:15:54 +0100
changeset 58830 e05c620eceeb
parent 58829 38340f6e971e
child 58831 aa8cf5eed06e
disable coercions for NO_MATCH
src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 29 19:26:05 2014 +0100
+++ b/src/HOL/HOL.thy	Thu Oct 30 09:15:54 2014 +0100
@@ -1692,8 +1692,11 @@
 *}
 
 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
+
 lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
 
+declare [[coercion_args NO_MATCH - -]]
+
 simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
   let
     val thy = Proof_Context.theory_of ctxt