src/HOL/Tools/meson.ML

   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
 fun forward_res nf st =
   let fun forward_tacf [prem] = rtac (nf prem) 1
         | forward_tacf prems =
             error ("Bad proof state in forward_res, please inform [e-mail]:\n" ^
-                   string_of_thm st ^
+                   Display.string_of_thm st ^
                    "\nPremises:\n" ^
-                   cat_lines (map string_of_thm prems))
+                   cat_lines (map Display.string_of_thm prems))
   in
     case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
     of SOME(th,_) => th
      | NONE => raise THM("forward_res", 0, [st])
   end;

               in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
           | _ => nodups th :: ths  (*no work to do*)
       and cnf_nil th = cnf_aux (th,[])
       val cls = 
 	    if too_many_clauses (SOME ctxt) (concl_of th)
-	    then (warning ("cnf is ignoring: " ^ string_of_thm th); ths)
+	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
 	    else cnf_aux (th,ths)
   in  (cls, !ctxtr)  end;
 
 fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
 

 
 fun skolemize_nnf_list [] = []
   | skolemize_nnf_list (th::ths) = 
       skolemize (make_nnf th) :: skolemize_nnf_list ths
       handle THM _ => (*RS can fail if Unify.search_bound is too small*)
-       (warning ("Failed to Skolemize " ^ string_of_thm th);
+       (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
         skolemize_nnf_list ths);
 
 fun add_clauses (th,cls) =
   let val ctxt0 = Variable.thm_context th
       val (cnfs,ctxt) = make_cnf [] th ctxt0

            [] => no_tac  (*no goal clauses*)
          | goes =>
              let val horns = make_horns (cls@ths)
                  val _ =
                      Output.debug (fn () => ("meson method called:\n" ^
-                                  space_implode "\n" (map string_of_thm (cls@ths)) ^
+                                  space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
                                   "\nclauses:\n" ^
-                                  space_implode "\n" (map string_of_thm horns)))
+                                  space_implode "\n" (map Display.string_of_thm horns)))
              in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
              end
  );
 
 fun meson_claset_tac ths cs =