# HG changeset patch
# User hoelzl
# Date 1414656954 -3600
# Node ID e05c620eceebb58f650edcb6354c2f5b653d92c7
# Parent  38340f6e971e0a6115a654756363017b6f6c5d7a
disable coercions for NO_MATCH

diff -r 38340f6e971e -r e05c620eceeb 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