# HG changeset patch
# User wenzelm
# Date 1420031106 -3600
# Node ID 663794ab87e60cf39e936aeff8b8e49a56c0c995
# Parent  0cbe0a56d3fabef3d61f9b60b21feaa79e0973a2
stripped ad-hoc diagnostic facility

diff -r 0cbe0a56d3fa -r 663794ab87e6 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Dec 31 11:27:26 2014 +1100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Dec 31 14:05:06 2014 +0100
@@ -8,15 +8,12 @@
 signature PREDICATE_COMPILE =
 sig
   val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory
-  val present_graph : bool Unsynchronized.ref
   val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
 struct
 
-val present_graph = Unsynchronized.ref false
-
 val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
 
 open Predicate_Compile_Aux;
@@ -142,7 +139,6 @@
         (fn () =>
           Predicate_Compile_Data.obtain_specification_graph options thy t
           |> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
-    val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
   in
     cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
       (fn () =>
diff -r 0cbe0a56d3fa -r 663794ab87e6 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Dec 31 11:27:26 2014 +1100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Dec 31 14:05:06 2014 +0100
@@ -16,7 +16,6 @@
   val obtain_specification_graph :
     Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
 
-  val present_graph : thm list Term_Graph.T -> unit
   val normalize_equation : theory -> thm -> thm
 end;
 
@@ -298,27 +297,4 @@
     extend t Term_Graph.empty
   end;
 
-
-fun present_graph gr =
-  let
-    fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
-    fun string_of_const (Const (c, _)) = c
-      | string_of_const _ = error "string_of_const: unexpected term"
-    val constss = Term_Graph.strong_conn gr;
-    val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
-      Termtab.update (const, consts)) consts) constss;
-    fun succs consts = consts
-      |> maps (Term_Graph.immediate_succs gr)
-      |> subtract eq_cname consts
-      |> map (the o Termtab.lookup mapping)
-      |> distinct (eq_list eq_cname);
-    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-
-    fun namify consts = map string_of_const consts
-      |> commas;
-    val prgr = map (fn (consts, constss) =>
-      {name = namify consts, ID = namify consts, dir = "", unfold = true,
-       path = "", parents = map namify constss, content = [] }) conn
-  in Graph_Display.display_graph prgr end
-
 end