1.1 --- a/src/HOL/Tools/meson.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -121,9 +121,9 @@
     1.4    let fun forward_tacf [prem] = rtac (nf prem) 1
     1.5          | forward_tacf prems =
     1.6              error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
     1.7 -                   string_of_thm st ^
     1.8 +                   Display.string_of_thm st ^
     1.9                     "\nPremises:\n" ^
    1.10 -                   cat_lines (map string_of_thm prems))
    1.11 +                   cat_lines (map Display.string_of_thm prems))
    1.12    in
    1.13      case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
    1.14      of SOME(th,_) => th
    1.15 @@ -335,7 +335,7 @@
    1.16        and cnf_nil th = cnf_aux (th,[])
    1.17        val cls = 
    1.18  	    if too_many_clauses (SOME ctxt) (concl_of th)
    1.19 -	    then (warning ("cnf is ignoring: " ^ string_of_thm th); ths)
    1.20 +	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
    1.21  	    else cnf_aux (th,ths)
    1.22    in  (cls, !ctxtr)  end;
    1.23  
    1.24 @@ -535,7 +535,7 @@
    1.25    | skolemize_nnf_list (th::ths) = 
    1.26        skolemize (make_nnf th) :: skolemize_nnf_list ths
    1.27        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
    1.28 -       (warning ("Failed to Skolemize " ^ string_of_thm th);
    1.29 +       (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
    1.30          skolemize_nnf_list ths);
    1.31  
    1.32  fun add_clauses (th,cls) =
    1.33 @@ -625,9 +625,9 @@
    1.34               let val horns = make_horns (cls@ths)
    1.35                   val _ =
    1.36                       Output.debug (fn () => ("meson method called:\n" ^
    1.37 -                                  space_implode "\n" (map string_of_thm (cls@ths)) ^
    1.38 +                                  space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
    1.39                                    "\nclauses:\n" ^
    1.40 -                                  space_implode "\n" (map string_of_thm horns)))
    1.41 +                                  space_implode "\n" (map Display.string_of_thm horns)))
    1.42               in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    1.43               end
    1.44   );