src/HOL/Probability/Probability_Measure.thy

--- a/src/HOL/Probability/Probability_Measure.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -239,16 +239,16 @@
 subsection  \<open>Introduce binder for probability\<close>
 
 syntax
-  "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'((/_ in _./ _)'))")
+  "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'((/_ in _./ _)'))\<close>)
 
 translations
   "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
 
 print_translation \<open>
   let
-    fun to_pattern (Const (@{const_syntax Pair}, _) $ l $ r) =
-      Syntax.const @{const_syntax Pair} :: to_pattern l @ to_pattern r
-    | to_pattern (t as (Const (@{syntax_const "_bound"}, _)) $ _) = [t]
+    fun to_pattern (Const (\<^const_syntax>\<open>Pair\<close>, _) $ l $ r) =
+      Syntax.const \<^const_syntax>\<open>Pair\<close> :: to_pattern l @ to_pattern r
+    | to_pattern (t as (Const (\<^syntax_const>\<open>_bound\<close>, _)) $ _) = [t]
 
     fun mk_pattern ((t, n) :: xs) = mk_patterns n xs |>> curry list_comb t
     and mk_patterns 0 xs = ([], xs)
@@ -261,32 +261,32 @@
       end
 
     fun unnest_tuples
-      (Const (@{syntax_const "_pattern"}, _) $
+      (Const (\<^syntax_const>\<open>_pattern\<close>, _) $
         t1 $
-        (t as (Const (@{syntax_const "_pattern"}, _) $ _ $ _)))
+        (t as (Const (\<^syntax_const>\<open>_pattern\<close>, _) $ _ $ _)))
       = let
         val (_ $ t2 $ t3) = unnest_tuples t
       in
-        Syntax.const @{syntax_const "_pattern"} $
+        Syntax.const \<^syntax_const>\<open>_pattern\<close> $
           unnest_tuples t1 $
-          (Syntax.const @{syntax_const "_patterns"} $ t2 $ t3)
+          (Syntax.const \<^syntax_const>\<open>_patterns\<close> $ t2 $ t3)
       end
     | unnest_tuples pat = pat
 
-    fun tr' [sig_alg, Const (@{const_syntax Collect}, _) $ t] =
+    fun tr' [sig_alg, Const (\<^const_syntax>\<open>Collect\<close>, _) $ t] =
       let
-        val bound_dummyT = Const (@{syntax_const "_bound"}, dummyT)
+        val bound_dummyT = Const (\<^syntax_const>\<open>_bound\<close>, dummyT)
 
         fun go pattern elem
-          (Const (@{const_syntax "conj"}, _) $
-            (Const (@{const_syntax Set.member}, _) $ elem' $ (Const (@{const_syntax space}, _) $ sig_alg')) $
+          (Const (\<^const_syntax>\<open>conj\<close>, _) $
+            (Const (\<^const_syntax>\<open>Set.member\<close>, _) $ elem' $ (Const (\<^const_syntax>\<open>space\<close>, _) $ sig_alg')) $
             u)
           = let
               val _ = if sig_alg aconv sig_alg' andalso to_pattern elem' = rev elem then () else raise Match;
               val (pat, rest) = mk_pattern (rev pattern);
               val _ = case rest of [] => () | _ => raise Match
             in
-              Syntax.const @{syntax_const "_prob"} $ unnest_tuples pat $ sig_alg $ u
+              Syntax.const \<^syntax_const>\<open>_prob\<close> $ unnest_tuples pat $ sig_alg $ u
             end
         | go pattern elem (Abs abs) =
             let
@@ -294,16 +294,16 @@
             in
               go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
             end
-        | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
+        | go pattern elem (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t) =
             go
-              ((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
-              (Syntax.const @{const_syntax Pair} :: elem)
+              ((Syntax.const \<^syntax_const>\<open>_pattern\<close>, 2) :: pattern)
+              (Syntax.const \<^const_syntax>\<open>Pair\<close> :: elem)
               t
       in
         go [] [] t
       end
   in
-    [(@{const_syntax Sigma_Algebra.measure}, K tr')]
+    [(\<^const_syntax>\<open>Sigma_Algebra.measure\<close>, K tr')]
   end
 \<close>
 
@@ -311,7 +311,7 @@
   "cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)"
 
 syntax
-  "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _ \<bar>/ _'))")
+  "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'(_ in _. _ \<bar>/ _'))\<close>)
 
 translations
   "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"