src/HOL/Tools/meson.ML

     "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   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" ^
-                   Display.string_of_thm st ^
-                   "\nPremises:\n" ^
-                   ML_Syntax.print_list Display.string_of_thm prems)
+            error (cat_lines
+              ("Bad proof state in forward_res, please inform [e-mail]:" ::
+                Display.string_of_thm_without_context st ::
+                "Premises:" :: map Display.string_of_thm_without_context 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: " ^ Display.string_of_thm th); ths)
+	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt 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 th :: skolemize_nnf_list ths
       handle THM _ => (*RS can fail if Unify.search_bound is too small*)
-       (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
+       (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
         skolemize_nnf_list ths);
 
 fun add_clauses (th,cls) =
   let val ctxt0 = Variable.thm_context th
       val (cnfs,ctxt) = make_cnf [] th ctxt0

 
 fun iter_deepen_prolog_tac horns =
     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
 
 fun iter_deepen_meson_tac ths = MESON make_clauses
- (fn cls =>
-      case (gocls (cls@ths)) of
-           [] => no_tac  (*no goal clauses*)
-         | goes =>
-             let val horns = make_horns (cls@ths)
-                 val _ =
-                     Output.debug (fn () => ("meson method called:\n" ^
-                                  ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
-                                  "\nclauses:\n" ^
-                                  ML_Syntax.print_list Display.string_of_thm horns))
-             in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
-             end
- );
+  (fn cls =>
+    (case (gocls (cls @ ths)) of
+      [] => no_tac  (*no goal clauses*)
+    | goes =>
+        let
+          val horns = make_horns (cls @ ths)
+          val _ = Output.debug (fn () =>
+            cat_lines ("meson method called:" ::
+              map Display.string_of_thm_without_context (cls @ ths) @
+              ["clauses:"] @ map Display.string_of_thm_without_context horns))
+        in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
 
 fun meson_claset_tac ths cs =
   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
 
 val meson_tac = meson_claset_tac [];