# HG changeset patch
# User wenzelm
# Date 1211117301 -7200
# Node ID c460ed6eeeef5a192f96583b80fbba648910a437
# Parent  df36f4c52ee8daa090920e7388ec15032cc5ef11
oops -- pr_graph = Syntax.string_of_term;
removed dead pr_matrix;

diff -r df36f4c52ee8 -r c460ed6eeeef src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Sun May 18 15:04:48 2008 +0200
+++ b/src/HOL/SizeChange/sct.ML	Sun May 18 15:28:21 2008 +0200
@@ -273,8 +273,6 @@
 fun dest_set (Const ("{}", _)) = []
   | dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs
 
-fun pr_matrix ctxt = map_matrix (fn Graph (G, _) => Syntax.string_of_term ctxt G | _ => "X")
-
 val in_graph_tac =
     simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
     THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
@@ -329,7 +327,7 @@
 
 
       val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
-                                                                            pr_graph ctxt G ^ ",\n")
+                                                                            Syntax.string_of_term ctxt G ^ ",\n")
                                                      | _ => I) cs) parts ""
       val _ = warning s