diff -r 6cc57bd46179 -r dab84266c85a src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 16:22:49 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 16:49:01 2025 +0100
@@ -387,9 +387,9 @@
       | process (#"M", [s]) = (fn state =>
           let
             val thy = get_theory state
-            val th = freeze thy (Global_Theory.get_thm thy s)
+            val th = Global_Theory.get_thm thy s
           in
-            set_thm th state
+            set_thm (freeze thy th) state
           end)
       | process (#"Q", l) = (fn state =>
           let
@@ -410,9 +410,10 @@
       | process (#"F", [name, t]) = (fn state =>
           let
             val (tm, state1) = term t state
-            val (th, state2) = map_theory_result (def (make_name name) tm) state1
           in
-            set_thm th state2
+            state1
+            |> map_theory_result (def (make_name name) tm)
+            |-> set_thm
           end)
       | process (#"F", [name]) = (fn state => set_thm (mdef (get_theory state) name) state)
       | process (#"Y", [name, absname, repname, t1, t2, th]) = (fn state =>
@@ -420,9 +421,10 @@
             val (th, state1) = thm th state
             val (t1, state2) = term t1 state1
             val (t2, state3) = term t2 state2
-            val (th, state4) = map_theory_result (tydef name absname repname t1 t2 th) state3
           in
-            set_thm th state4
+            state3
+            |> map_theory_result (tydef name absname repname t1 t2 th)
+            |-> set_thm
           end)
       | process (#"Y", [name, _, _]) = (fn state => set_thm (mtydef (get_theory state) name) state)
       | process (#"t", [n]) = (fn state => set_typ (ctyp_of state (make_tfree n)) state)