# HG changeset patch
# User wenzelm
# Date 1684060489 -7200
# Node ID 6200555461c65450da22182b40aa9b4364672cec
# Parent  9da707dad2a350b5901cda98ebd669fc068cc7a4
proper Thm.trim_context / Thm.transfer;

diff -r 9da707dad2a3 -r 6200555461c6 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sat May 13 21:30:34 2023 +0200
+++ b/src/HOL/Statespace/state_space.ML	Sun May 14 12:34:49 2023 +0200
@@ -228,12 +228,14 @@
   else (tracing ("variable not fixed or declared: " ^ name); NONE)
 
 
-val get_dist_thm = Symtab.lookup o get_distinctthm;
+fun get_dist_thm context name =
+  Symtab.lookup_list (get_distinctthm context) name
+  |> map (Thm.transfer'' context)
 
 fun get_dist_thm2 ctxt x y =
  (let
     val dist_thms = [x, y] |> map (#1 o dest_Free)
-      |> map (these o get_dist_thm (Context.Proof ctxt)) |> flat;
+      |> maps (get_dist_thm (Context.Proof ctxt));
 
     fun get_paths dist_thm =
       let
@@ -331,7 +333,8 @@
           val declinfo = get_declinfo context
           val tt = get_distinctthm context;
           val all_names = comps_of_distinct_thm thm;
-          fun upd name = Symtab.map_default (name, [thm]) (insert_distinct_thm thm)
+          val thm0 = Thm.trim_context thm;
+          fun upd name = Symtab.map_default (name, [thm0]) (insert_distinct_thm thm0)
 
           val tt' = tt |> fold upd all_names;
           val context' =