src/HOL/Tools/Meson/meson.ML
changeset 59621 291934bac95e
parent 59617 b60e65ad13df
child 59632 5980e75a204e
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4            val tenv =
     1.5              Pattern.first_order_match thy (tmB, tmA)
     1.6                                            (Vartab.empty, Vartab.empty) |> snd
     1.7 -          val ct_pairs = map (apply2 (Thm.cterm_of thy) o term_pair_of) (Vartab.dest tenv)
     1.8 +          val ct_pairs = map (apply2 (Thm.global_cterm_of thy) o term_pair_of) (Vartab.dest tenv)
     1.9        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    1.10      SOME th => th
    1.11    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    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.cterm_of (Thm.theory_of_thm th) c
    1.17 +      val cc = Thm.global_cterm_of (Thm.theory_of_thm th) 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 @@ -355,7 +355,7 @@
    1.22        val ([x], ctxt') =
    1.23          Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
    1.24        val spec' = spec
    1.25 -        |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
    1.26 +        |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, spec_varT)))]);
    1.27      in (th RS spec', ctxt') end
    1.28  end;
    1.29  
    1.30 @@ -629,7 +629,7 @@
    1.31             $ (t as _ $ _) $ (u as _ $ _))) =>
    1.32      (case get_F_pattern T t u of
    1.33         SOME p =>
    1.34 -       let val inst = [apply2 (Thm.cterm_of thy) (F_ext_cong_neq, p)] in
    1.35 +       let val inst = [apply2 (Thm.global_cterm_of thy) (F_ext_cong_neq, p)] in
    1.36           th RS cterm_instantiate inst ext_cong_neq
    1.37         end
    1.38       | NONE => th)