# HG changeset patch
# User wenzelm
# Date 1635534368 -7200
# Node ID 8ab92e40dde6d55957049bac0615d97709d257c4
# Parent  f1099c7330b7cf9e9f39d020c8043521fbd8f30e
clarified antiquotations;

diff -r f1099c7330b7 -r 8ab92e40dde6 src/HOL/Analysis/measurable.ML
--- a/src/HOL/Analysis/measurable.ML	Fri Oct 29 20:39:16 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML	Fri Oct 29 21:06:08 2021 +0200
@@ -129,15 +129,15 @@
 
 fun dest_measurable_fun t =
   (case t of
-    (Const (\<^const_name>\<open>Set.member\<close>, _) $ f $ (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _)) => f
+    \<^Const_>\<open>Set.member _ for f \<^Const_>\<open>measurable _ _ for _ _\<close>\<close> => f
   | _ => raise (TERM ("not a measurability predicate", [t])))
 
 fun not_measurable_prop n thm =
   if length (Thm.prems_of thm) < n then false
   else
     (case nth_hol_goal thm n of
-      (Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ (Const (\<^const_name>\<open>sets\<close>, _) $ _)) => false
-    | (Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _)) => false
+      \<^Const_>\<open>Set.member _ for _ \<^Const_>\<open>sets _ for _\<close>\<close> => false
+    | \<^Const_>\<open>Set.member _ for _ \<^Const_>\<open>measurable _ _ for _ _\<close>\<close> => false
     | _ => true)
     handle TERM _ => true;
 
@@ -214,16 +214,12 @@
           THEN' K (debug_tac ctxt (debug_fact (msg ^ " resolved using") thm) all_tac))
       else resolve_tac ctxt
 
-    val elem_congI = @{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}
-
     val (thms, ctxt) = prepare_facts ctxt facts
 
-    fun is_sets_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
-          (Const (\<^const_name>\<open>sets\<close>, _) $ _) $
-          (Const (\<^const_name>\<open>sets\<close>, _) $ _)) = true
-      | is_sets_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
-          (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _) $
-          (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _)) = true
+    fun is_sets_eq \<^Const_>\<open>HOL.eq _ for
+          \<^Const_>\<open>sets _ for _\<close> \<^Const_>\<open>sets _ for _\<close>\<close> = true
+      | is_sets_eq \<^Const_>\<open>HOL.eq _ for
+          \<^Const_>\<open>measurable _ _ for _ _\<close> \<^Const_>\<open>measurable _ _ for _ _\<close>\<close> = true
       | is_sets_eq _ = false
 
     val cong_thms = get_cong (Context.Proof ctxt) @
@@ -234,7 +230,7 @@
         let
           val ctxt'' = Simplifier.add_prems prems ctxt'
         in
-          r_tac "cong intro" [elem_congI]
+          r_tac "cong intro" [@{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}]
           THEN' SOLVED' (fn i => REPEAT_DETERM (
               ((r_tac "cong solve" (cong_thms @ [@{thm refl}])
                 ORELSE' IF' (fn i => fn thm => Thm.nprems_of thm > i)