# HG changeset patch
# User wenzelm
# Date 1368281588 -7200
# Node ID 5e8a0b8bb070c64155ad7340421bfbb4c6c72b76
# Parent  bcd6898ac613a9b214d409dbf98c4f02979d129e
avoid PolyML.makestring, even in dead code;

diff -r bcd6898ac613 -r 5e8a0b8bb070 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Fri May 10 19:41:23 2013 +0200
+++ b/src/HOL/Library/Debug.thy	Sat May 11 16:13:08 2013 +0200
@@ -30,6 +30,7 @@
   [simp]: "timing s f x = f x"
 
 code_const trace and flush and timing
+  (* FIXME proper @{make_string} instead of PolyML.makestring?!?! *)
   (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
 
 code_reserved Eval Output PolyML Timing
diff -r bcd6898ac613 -r 5e8a0b8bb070 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Fri May 10 19:41:23 2013 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Sat May 11 16:13:08 2013 +0200
@@ -56,7 +56,7 @@
   let
     fun tac [] st = all_tac st
       | tac (type_enc :: type_encs) st =
-        st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
+        st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *)
            |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
                THEN Metis_Tactic.metis_tac [type_enc]
                     ATP_Problem_Generate.combsN ctxt ths 1
diff -r bcd6898ac613 -r 5e8a0b8bb070 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri May 10 19:41:23 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat May 11 16:13:08 2013 +0200
@@ -722,12 +722,12 @@
 (* for debugging only:
       fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
-        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
+        "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
-      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
-      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
-      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
+      val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters)
+      val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
+      val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        cat_lines (map string_for_subst_info substs))
 *)