# HG changeset patch
# User wenzelm
# Date 1409233910 -7200
# Node ID 27ee844c2b4dff4f4a35f073128a2945189995de
# Parent  0255436b3d859b74db55b8582ce4a01b56795a28
tuned;

diff -r 0255436b3d85 -r 27ee844c2b4d src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 28 15:47:26 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 28 15:51:50 2014 +0200
@@ -323,7 +323,7 @@
   let val thy = Proof_Context.theory_of ctxt
       val m_tm = Metis_Term.Fn atom
       val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
-      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos)
+      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
       fun path_finder_fail tm ps t =