# HG changeset patch
# User wenzelm
# Date 1211115860 -7200
# Node ID fe007ee497c1baffa7cd761593a4cd724ac032fc
# Parent  80df961f790063328f2d077424741b1be9449670
pr_matrix: proper context;

diff -r 80df961f7900 -r fe007ee497c1 src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Sun May 18 15:04:17 2008 +0200
+++ b/src/HOL/SizeChange/sct.ML	Sun May 18 15:04:20 2008 +0200
@@ -273,8 +273,7 @@
 fun dest_set (Const ("{}", _)) = []
   | dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs
 
-val pr_graph = Sign.string_of_term
-fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X")
+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
@@ -330,9 +329,9 @@
 
 
       val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
-                                                                            pr_graph thy G ^ ",\n")
+                                                                            pr_graph ctxt G ^ ",\n")
                                                      | _ => I) cs) parts ""
-      val _ = Output.warning s
+      val _ = warning s
 
 
       val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)