# HG changeset patch
# User hoelzl
# Date 1427119682 -3600
# Node ID b6bda9140e39eed09e3211fb96bcfacc5bf1a28f
# Parent  fe5b796d6b2a9e5be9546bc28a794fb230a735e0
fix parameter order of NO_MATCH

diff -r fe5b796d6b2a -r b6bda9140e39 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Fields.thy	Mon Mar 23 15:08:02 2015 +0100
@@ -30,8 +30,8 @@
 begin
 
 lemma [field_simps]:
-  shows distrib_left_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b + c) = a * b + a * c"
-    and distrib_right_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a + b) * c = a * c + b * c"
+  shows distrib_left_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   by (rule distrib_left distrib_right)+
 
 end
@@ -40,8 +40,8 @@
 begin
 
 lemma [field_simps]:
-  shows left_diff_distrib_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a - b) * c = a * c - b * c"
-    and right_diff_distrib_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b - c) = a * b - a * c"
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   by (rule left_diff_distrib right_diff_distrib)+
 
 end
diff -r fe5b796d6b2a -r b6bda9140e39 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/HOL.thy	Mon Mar 23 15:08:02 2015 +0100
@@ -1671,13 +1671,13 @@
  The simplification procedure can be used to avoid simplification of terms of a certain form
 *}
 
-definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
 
-lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
+lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
 
 declare [[coercion_args NO_MATCH - -]]
 
-simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
+simproc_setup NO_MATCH ("NO_MATCH pat val") = {* fn _ => fn ctxt => fn ct =>
   let
     val thy = Proof_Context.theory_of ctxt
     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
@@ -1686,7 +1686,7 @@
 *}
 
 text {*
-  This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
+  This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
   is only applied, if the pattern @{term pat} does not match the value @{term val}.
 *}
 
diff -r fe5b796d6b2a -r b6bda9140e39 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Mar 23 15:08:02 2015 +0100
@@ -1955,7 +1955,7 @@
 qed
 
 lemma nn_integral_count_space_indicator:
-  assumes "NO_MATCH (X::'a set) (UNIV::'a set)"
+  assumes "NO_MATCH (UNIV::'a set) (X::'a set)"
   shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
   by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)