1.1 --- a/src/HOL/Tools/meson.ML	Tue Sep 09 16:15:25 2008 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Sep 09 16:16:20 2008 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4              error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
     1.5                     Display.string_of_thm st ^
     1.6                     "\nPremises:\n" ^
     1.7 -                   cat_lines (map Display.string_of_thm prems))
     1.8 +                   ML_Syntax.print_list Display.string_of_thm prems)
     1.9    in
    1.10      case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
    1.11      of SOME(th,_) => th
    1.12 @@ -495,10 +495,10 @@
    1.13  fun make_nnf1 th =
    1.14    if ok4nnf (concl_of th)
    1.15    then make_nnf1 (tryres(th, nnf_rls))
    1.16 -    handle THM _ =>
    1.17 +    handle THM ("tryres", _, _) =>
    1.18          forward_res make_nnf1
    1.19             (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
    1.20 -    handle THM _ => th
    1.21 +    handle THM ("tryres", _, _) => th
    1.22    else th;
    1.23  
    1.24  (*The simplification removes defined quantifiers and occurrences of True and False.
    1.25 @@ -526,10 +526,11 @@
    1.26    if not (has_conns ["Ex"] (prop_of th)) then th
    1.27    else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    1.28                                disj_exD, disj_exD1, disj_exD2])))
    1.29 -    handle THM _ =>
    1.30 +    handle THM ("tryres", _, _) =>
    1.31          skolemize (forward_res skolemize
    1.32                     (tryres (th, [conj_forward, disj_forward, all_forward])))
    1.33 -    handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
    1.34 +    handle THM ("tryres", _, _) => 
    1.35 +        forward_res skolemize (rename_bvs_RS th ex_forward);
    1.36  
    1.37  fun skolemize_nnf_list [] = []
    1.38    | skolemize_nnf_list (th::ths) = 
    1.39 @@ -625,9 +626,9 @@
    1.40               let val horns = make_horns (cls@ths)
    1.41                   val _ =
    1.42                       Output.debug (fn () => ("meson method called:\n" ^
    1.43 -                                  cat_lines (map Display.string_of_thm (cls@ths)) ^
    1.44 +                                  ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
    1.45                                    "\nclauses:\n" ^
    1.46 -                                  cat_lines (map Display.string_of_thm horns)))
    1.47 +                                  ML_Syntax.print_list Display.string_of_thm horns))
    1.48               in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    1.49               end
    1.50   );