src/HOL/Tools/Meson/meson.ML
changeset 60781 2da59cdf531c
parent 60696 8304fb4fb823
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  sig
     1.5    val trace : bool Config.T
     1.6    val max_clauses : int Config.T
     1.7 -  val term_pair_of: indexname * (typ * 'a) -> term * 'a
     1.8    val first_order_resolve : Proof.context -> thm -> thm -> thm
     1.9    val size_of_subgoals: thm -> int
    1.10    val has_too_many_clauses: Proof.context -> term -> bool
    1.11 @@ -95,8 +94,6 @@
    1.12  
    1.13  (** First-order Resolution **)
    1.14  
    1.15 -fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    1.16 -
    1.17  (*FIXME: currently does not "rename variables apart"*)
    1.18  fun first_order_resolve ctxt thA thB =
    1.19    (case
    1.20 @@ -107,8 +104,8 @@
    1.21            val tenv =
    1.22              Pattern.first_order_match thy (tmB, tmA)
    1.23                                            (Vartab.empty, Vartab.empty) |> snd
    1.24 -          val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
    1.25 -      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    1.26 +          val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv [];
    1.27 +      in  thA RS (infer_instantiate ctxt insts thB) end) () of
    1.28      SOME th => th
    1.29    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    1.30  
    1.31 @@ -616,10 +613,6 @@
    1.32    handle NO_F_PATTERN () => NONE
    1.33  
    1.34  val ext_cong_neq = @{thm ext_cong_neq}
    1.35 -val F_ext_cong_neq =
    1.36 -  Term.add_vars (Thm.prop_of @{thm ext_cong_neq}) []
    1.37 -  |> filter (fn ((s, _), _) => s = "F")
    1.38 -  |> the_single |> Var
    1.39  
    1.40  (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    1.41  fun cong_extensionalize_thm ctxt th =
    1.42 @@ -628,11 +621,8 @@
    1.43          $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
    1.44             $ (t as _ $ _) $ (u as _ $ _))) =>
    1.45      (case get_F_pattern T t u of
    1.46 -       SOME p =>
    1.47 -       let val inst = [apply2 (Thm.cterm_of ctxt) (F_ext_cong_neq, p)] in
    1.48 -         th RS cterm_instantiate inst ext_cong_neq
    1.49 -       end
    1.50 -     | NONE => th)
    1.51 +      SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
    1.52 +    | NONE => th)
    1.53    | _ => th)
    1.54  
    1.55  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It