# 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