src/HOL/Tools/Meson/meson_clausify.ML
changeset 39941 02fcd9cd1eac
parent 39940 1f01c9b2b76b
child 39948 317010af8972
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 04 21:37:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 04 21:49:07 2010 +0200
     1.3 @@ -1,8 +1,9 @@
     1.4 -(*  Title:      HOL/Tools/Sledgehammer/meson_clausify.ML
     1.5 +(*  Title:      HOL/Tools/Meson/meson_clausify.ML
     1.6      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.7      Author:     Jasmin Blanchette, TU Muenchen
     1.8  
     1.9 -Transformation of axiom rules (elim/intro/etc) into CNF forms.
    1.10 +Transformation of HOL theorems into CNF forms.
    1.11 +The "meson" proof method for HOL.
    1.12  *)
    1.13  
    1.14  signature MESON_CLAUSIFY =
    1.15 @@ -204,7 +205,7 @@
    1.16      val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
    1.17      val T =
    1.18        case hilbert of
    1.19 -        Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
    1.20 +        Const (_, Type (@{type_name fun}, [_, T])) => T
    1.21        | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
    1.22                           [hilbert])
    1.23      val cex = cterm_of thy (HOLogic.exists_const T)
    1.24 @@ -214,7 +215,8 @@
    1.25        |> Drule.beta_conv cabs |> Thm.capply cTrueprop
    1.26      fun tacf [prem] =
    1.27        rewrite_goals_tac skolem_def_raw
    1.28 -      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
    1.29 +      THEN rtac ((prem |> rewrite_rule skolem_def_raw)
    1.30 +                 RS Global_Theory.get_thm thy "someI_ex") 1
    1.31    in
    1.32      Goal.prove_internal [ex_tm] conc tacf
    1.33      |> forall_intr_list frees