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
```