--- a/src/HOL/Statespace/state_fun.ML Mon Oct 25 23:10:06 2021 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Nov 12 17:01:52 2020 +0100
@@ -16,6 +16,8 @@
val ex_lookup_ss : simpset
val lazy_conj_simproc : simproc
val string_eq_simp_tac : Proof.context -> int -> tactic
+
+ val trace_data : Context.generic -> unit
end;
structure StateFun: STATE_FUN =
@@ -105,6 +107,17 @@
(merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
);
+fun trace_data context =
+ let
+ val (lookup_ss, ex_ss, active) = Data.get context
+ val pretty_ex_ss = Simplifier.pretty_simpset true (put_simpset ex_ss (Context.proof_of context))
+ val pretty_lookup_ss = Simplifier.pretty_simpset true (put_simpset lookup_ss (Context.proof_of context))
+ in
+ tracing ("state_fun ex_ss: " ^ Pretty.string_of pretty_ex_ss ^
+ "\n ================= \n lookup_ss: " ^ Pretty.string_of pretty_lookup_ss ^ "\n " ^
+ "active: " ^ @{make_string} active)
+ end
+
val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)));
val lookup_simproc =