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