src/HOL/Tools/Meson/meson_clausify.ML
changeset 42747 f132d13fcf75
parent 42739 017e5dac8642
child 42944 9e620869a576
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4    val new_skolem_var_prefix : string
     1.5    val new_nonskolem_var_prefix : string
     1.6    val is_zapped_var_name : string -> bool
     1.7 -  val extensionalize_theorem : thm -> thm
     1.8    val introduce_combinators_in_cterm : cterm -> thm
     1.9    val introduce_combinators_in_theorem : thm -> thm
    1.10    val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    1.11 @@ -87,16 +86,6 @@
    1.12  
    1.13  (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    1.14  
    1.15 -val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
    1.16 -
    1.17 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
    1.18 -   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    1.19 -fun extensionalize_theorem th =
    1.20 -  case prop_of th of
    1.21 -    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
    1.22 -         $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
    1.23 -  | _ => th
    1.24 -
    1.25  fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true
    1.26    | is_quasi_lambda_free (t1 $ t2) =
    1.27      is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
    1.28 @@ -321,7 +310,7 @@
    1.29      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
    1.30      val th = th |> Conv.fconv_rule Object_Logic.atomize
    1.31                  |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
    1.32 -                |> extensionalize_theorem
    1.33 +                |> extensionalize_theorem ctxt
    1.34                  |> make_nnf ctxt
    1.35    in
    1.36      if new_skolemizer then