# HG changeset patch
# User wenzelm
# Date 1682083859 -7200
# Node ID 5728d5ebce34e8be622701d7b746653c737fdde0
# Parent  42214742b44a8b915c47e0e158c072d297133e8a
more uniform operations wrt. Thm.full_prop_of;

diff -r 42214742b44a -r 5728d5ebce34 src/HOL/Analysis/measurable.ML
--- a/src/HOL/Analysis/measurable.ML	Fri Apr 21 15:26:11 2023 +0200
+++ b/src/HOL/Analysis/measurable.ML	Fri Apr 21 15:30:59 2023 +0200
@@ -54,7 +54,7 @@
     (*cong_thms*) thm Item_Net.T *
     (string * preprocessor) list
   val empty: T =
-    (Item_Net.init eq_measurable_thm (single o Thm.prop_of o fst), Thm.item_net, Thm.item_net, [])
+    (Item_Net.init eq_measurable_thm (single o Thm.full_prop_of o fst), Thm.item_net, Thm.item_net, [])
   fun merge
    ((measurable_thms1, dest_thms1, cong_thms1, preprocessors1),
     (measurable_thms2, dest_thms2, cong_thms2, preprocessors2)) : T =
@@ -82,7 +82,7 @@
 
 fun del_thm th net =
   let
-    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
+    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm_prop (th, th'))
   in fold Item_Net.remove thms net end ;
 
 fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute