--- 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' =