equal
deleted
inserted
replaced
216 |
216 |
217 val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); |
217 val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); |
218 |
218 |
219 fun trace ctxt rules = |
219 fun trace ctxt rules = |
220 if Config.get ctxt rule_trace andalso not (null rules) then |
220 if Config.get ctxt rule_trace andalso not (null rules) then |
221 Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) |
221 Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules) |
222 |> Pretty.string_of |> tracing |
222 |> Pretty.string_of |> tracing |
223 else (); |
223 else (); |
224 |
224 |
225 local |
225 local |
226 |
226 |