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