# HG changeset patch
# User blanchet
# Date 1502802457 -7200
# Node ID d14e7666d785a97c28636f81dd0b24d6c0b11319
# Parent  a5dd01b682189f5412460b78b9611f7665b26894
added debugging function

diff -r a5dd01b68218 -r d14e7666d785 src/HOL/Tools/SMT/z3_proof.ML
--- a/src/HOL/Tools/SMT/z3_proof.ML	Tue Aug 15 11:52:17 2017 +0200
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Tue Aug 15 15:07:37 2017 +0200
@@ -118,6 +118,18 @@
 fun mk_node id rule prems concl bounds =
   Z3_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
 
+fun string_of_node ctxt =
+  let
+    fun str depth (Z3_Node {id, rule, prems, concl, bounds}) =
+      replicate_string depth "  " ^
+      enclose "{" "}" (commas
+        [string_of_int id,
+         string_of_rule rule,
+         enclose "[" "]" (space_implode " " bounds),
+         Syntax.string_of_term ctxt concl] ^
+        cat_lines (map (prefix "\n" o str (depth + 1)) prems))
+  in str 0 end
+
 datatype z3_step = Z3_Step of {
   id: int,
   rule: z3_rule,