src/HOL/Tools/Meson/meson.ML
changeset 61268 abe08fb15a12
parent 60801 7664e0916eec
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Sep 25 20:04:25 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Sep 25 20:37:59 2015 +0200
     1.3 @@ -186,8 +186,8 @@
     1.4        | tacf prems =
     1.5          error (cat_lines
     1.6            ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
     1.7 -            Display.string_of_thm ctxt st ::
     1.8 -            "Premises:" :: map (Display.string_of_thm ctxt) prems))
     1.9 +            Thm.string_of_thm ctxt st ::
    1.10 +            "Premises:" :: map (Thm.string_of_thm ctxt) prems))
    1.11    in
    1.12      case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of
    1.13        SOME (th, _) => th
    1.14 @@ -395,7 +395,7 @@
    1.15        val cls =
    1.16          if has_too_many_clauses ctxt (Thm.concl_of th) then
    1.17            (trace_msg ctxt (fn () =>
    1.18 -               "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.19 +               "cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths)
    1.20          else
    1.21            cnf_aux (th, ths)
    1.22    in (cls, !ctxt_ref) end
    1.23 @@ -652,7 +652,7 @@
    1.24                                 |> tap (fn NONE =>
    1.25                                            trace_msg ctxt (fn () =>
    1.26                                                "Failed to skolemize " ^
    1.27 -                                               Display.string_of_thm ctxt th)
    1.28 +                                               Thm.string_of_thm ctxt th)
    1.29                                          | _ => ()))
    1.30    end
    1.31  
    1.32 @@ -751,8 +751,8 @@
    1.33            val horns = make_horns (cls @ ths)
    1.34            val _ = trace_msg ctxt (fn () =>
    1.35              cat_lines ("meson method called:" ::
    1.36 -              map (Display.string_of_thm ctxt) (cls @ ths) @
    1.37 -              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    1.38 +              map (Thm.string_of_thm ctxt) (cls @ ths) @
    1.39 +              ["clauses:"] @ map (Thm.string_of_thm ctxt) horns))
    1.40          in
    1.41            THEN_ITER_DEEPEN iter_deepen_limit
    1.42              (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)