src/HOL/Tools/Meson/meson.ML
changeset 59632 5980e75a204e
parent 59621 291934bac95e
child 60358 aebfbcab1eb8
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 23:44:51 2015 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 23:44:57 2015 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    val choice_theorems : theory -> thm list
     1.5    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
     1.6    val skolemize : Proof.context -> thm -> thm
     1.7 -  val cong_extensionalize_thm : theory -> thm -> thm
     1.8 +  val cong_extensionalize_thm : Proof.context -> thm -> thm
     1.9    val abs_extensionalize_conv : Proof.context -> conv
    1.10    val abs_extensionalize_thm : Proof.context -> thm -> thm
    1.11    val make_clauses_unsorted: Proof.context -> thm list -> thm list
    1.12 @@ -174,7 +174,7 @@
    1.13    case (Thm.concl_of st, Thm.prop_of th) of
    1.14      (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    1.15      let
    1.16 -      val cc = Thm.global_cterm_of (Thm.theory_of_thm th) c
    1.17 +      val cc = Thm.cterm_of ctxt c
    1.18        val ct = Thm.dest_arg (Thm.cprop_of th)
    1.19      in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.20    | _ => resolve_tac ctxt [th] i st
    1.21 @@ -622,14 +622,14 @@
    1.22    |> the_single |> Var
    1.23  
    1.24  (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    1.25 -fun cong_extensionalize_thm thy th =
    1.26 +fun cong_extensionalize_thm ctxt th =
    1.27    (case Thm.concl_of th of
    1.28      @{const Trueprop} $ (@{const Not}
    1.29          $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
    1.30             $ (t as _ $ _) $ (u as _ $ _))) =>
    1.31      (case get_F_pattern T t u of
    1.32         SOME p =>
    1.33 -       let val inst = [apply2 (Thm.global_cterm_of thy) (F_ext_cong_neq, p)] in
    1.34 +       let val inst = [apply2 (Thm.cterm_of ctxt) (F_ext_cong_neq, p)] in
    1.35           th RS cterm_instantiate inst ext_cong_neq
    1.36         end
    1.37       | NONE => th)
    1.38 @@ -651,8 +651,7 @@
    1.39  
    1.40  fun try_skolemize_etc ctxt th =
    1.41    let
    1.42 -    val thy = Proof_Context.theory_of ctxt
    1.43 -    val th = th |> cong_extensionalize_thm thy
    1.44 +    val th = th |> cong_extensionalize_thm ctxt
    1.45    in
    1.46      [th]
    1.47      (* Extensionalize lambdas in "th", because that makes sense and that's what