# HG changeset patch
# User wenzelm
# Date 1737201203 -3600
# Node ID d596c7fc7d4b084a24c4bcca717c81f37f0ba6c0
# Parent  93b32361d398cf7ec9188bb345735f9de6007d6e
clarified signature;

diff -r 93b32361d398 -r d596c7fc7d4b src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sat Jan 18 12:45:33 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Sat Jan 18 12:53:23 2025 +0100
@@ -348,11 +348,13 @@
 fun set_term tm (State (thy, a, b, c)) = State (thy, a, set b tm, c)
 fun set_thm th (State (thy, a, b, c)) = State (thy, a, b, set c th)
 
-fun get_thm name (state as State (thy, _, _, _)) =
-  (freeze thy (Global_Theory.get_thm thy name), state);
+fun stored_thm name (State (thy, a, b, c)) =
+  let val th = freeze thy (Global_Theory.get_thm thy name)
+  in State (thy, a, b, set c th) end
 
-fun store_last_thm binding (State (thy, a, b, c as (tab, no))) =
+fun store_thm name (State (thy, a, b, c as (tab, no))) =
   let
+    val binding = Binding.name (make_name name)
     val th0 =
       (case Inttab.lookup tab no of
         NONE => raise Fail ("No thm " ^ string_of_int no)
@@ -390,7 +392,7 @@
   | command (#"E", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry eq_mp #-> set_thm
   | command (#"D", [th1, th2]) = thm th1 ##>> thm th2 #>> uncurry deduct #-> set_thm
   | command (#"L", [t, th]) = term t ##>> thm th #>> uncurry abs #-> set_thm
-  | command (#"M", [s]) = get_thm s #-> set_thm
+  | command (#"M", [name]) = stored_thm name
   | command (#"Q", args) =
       split_last args |> (fn (tys, th) => thm th #-> (fn th => typs tys #-> (fn tys =>
         set_thm (inst_type (pair_list tys) th))))
@@ -410,7 +412,7 @@
   | command (#"c", [c, ty]) = theory #-> (fn thy => typ ty #>> make_const thy c #-> set_term)
   | command (#"f", [t, u]) = term t #-> (fn t => term u #-> (fn u => set_term (Thm.apply t u)))
   | command (#"l", [x, t]) = term x #-> (fn x => term t #-> (fn t => set_term (Thm.lambda x t)))
-  | command (#"+", [s]) = store_last_thm (Binding.name (make_name s))
+  | command (#"+", [name]) = store_thm name
   | command (c, _) = raise Fail ("process: unknown command: " ^ String.str c)
 
 in