--- 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
--- 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
--- 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))
*)