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 );