src/HOL/Tools/Lifting/lifting_def.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59630 c9aa1c90796f
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  fun try_prove_reflexivity ctxt prop =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 -    val cprop = Thm.cterm_of thy prop
     1.8 +    val cprop = Thm.global_cterm_of thy prop
     1.9      val rule = @{thm ge_eq_refl}
    1.10      val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule)
    1.11      val insts = Thm.first_order_match (concl_pat, cprop)
    1.12 @@ -99,7 +99,7 @@
    1.13            end;
    1.14          
    1.15          val subst = fold make_subst free_vars [];
    1.16 -        val csubst = map (apply2 (Thm.cterm_of thy)) subst;
    1.17 +        val csubst = map (apply2 (Thm.global_cterm_of thy)) subst;
    1.18          val inst_thm = Drule.cterm_instantiate csubst thm;
    1.19        in
    1.20          Conv.fconv_rule 
    1.21 @@ -112,13 +112,13 @@
    1.22        let
    1.23          val t1 = (HOLogic.dest_Trueprop o Thm.concl_of) ant1
    1.24          val t2 = (HOLogic.dest_Trueprop o Thm.prop_of) ant2
    1.25 -        val fun1 = Thm.cterm_of thy (strip_args 2 t1)
    1.26 -        val args1 = map (Thm.cterm_of thy) (get_args 2 t1)
    1.27 -        val fun2 = Thm.cterm_of thy (strip_args 2 t2)
    1.28 -        val args2 = map (Thm.cterm_of thy) (get_args 1 t2)
    1.29 +        val fun1 = Thm.global_cterm_of thy (strip_args 2 t1)
    1.30 +        val args1 = map (Thm.global_cterm_of thy) (get_args 2 t1)
    1.31 +        val fun2 = Thm.global_cterm_of thy (strip_args 2 t2)
    1.32 +        val args2 = map (Thm.global_cterm_of thy) (get_args 1 t2)
    1.33          val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
    1.34          val vars = (rev (Term.add_vars (Thm.prop_of relcomppI) []))
    1.35 -        val subst = map (apfst (Thm.cterm_of thy o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
    1.36 +        val subst = map (apfst (Thm.global_cterm_of thy o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
    1.37        in
    1.38          Drule.cterm_instantiate subst relcomppI
    1.39        end
    1.40 @@ -129,10 +129,10 @@
    1.41          fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
    1.42          val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
    1.43          val typ = Thm.typ_of_cterm rel
    1.44 -        val POS_const = Thm.cterm_of thy (mk_POS typ)
    1.45 -        val var = Thm.cterm_of thy (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
    1.46 +        val POS_const = Thm.global_cterm_of thy (mk_POS typ)
    1.47 +        val var = Thm.global_cterm_of thy (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
    1.48          val goal =
    1.49 -          Thm.apply (Thm.cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
    1.50 +          Thm.apply (Thm.global_cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
    1.51        in
    1.52          [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
    1.53        end
    1.54 @@ -216,7 +216,7 @@
    1.55      val (var_name, T) = dest_abs (Thm.term_of rhs)
    1.56      val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
    1.57      val thy = Proof_Context.theory_of ctxt'
    1.58 -    val refl_thm = Thm.reflexive (Thm.cterm_of thy (Free (hd new_var_names, T)))
    1.59 +    val refl_thm = Thm.reflexive (Thm.global_cterm_of thy (Free (hd new_var_names, T)))
    1.60    in
    1.61      Thm.combination def refl_thm |>
    1.62      singleton (Proof_Context.export ctxt' ctxt)
    1.63 @@ -301,7 +301,7 @@
    1.64            SOME mono_eq_thm =>
    1.65              let
    1.66                val rep_abs_eq = mono_eq_thm RS rep_abs_thm
    1.67 -              val rep = (Thm.cterm_of thy o quot_thm_rep) quot_thm
    1.68 +              val rep = (Thm.global_cterm_of thy o quot_thm_rep) quot_thm
    1.69                val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
    1.70                val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
    1.71                val code_cert = [repped_eq, rep_abs_eq] MRSL trans
    1.72 @@ -380,7 +380,7 @@
    1.73  local
    1.74    fun encode_code_eq thy abs_eq opt_rep_eq (rty, qty) = 
    1.75      let
    1.76 -      fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of thy |> Drule.mk_term
    1.77 +      fun mk_type typ = typ |> Logic.mk_type |> Thm.global_cterm_of thy |> Drule.mk_term
    1.78      in
    1.79        Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
    1.80      end
    1.81 @@ -497,7 +497,7 @@
    1.82  in
    1.83  fun mk_readable_rsp_thm_eq tm lthy =
    1.84    let
    1.85 -    val ctm = Proof_Context.cterm_of lthy tm
    1.86 +    val ctm = Thm.cterm_of lthy tm
    1.87      
    1.88      fun assms_rewr_conv tactic rule ct =
    1.89        let
    1.90 @@ -622,7 +622,7 @@
    1.91      val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
    1.92        (Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)))
    1.93      val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
    1.94 -      |> Proof_Context.cterm_of lthy
    1.95 +      |> Thm.cterm_of lthy
    1.96        |> cr_to_pcr_conv
    1.97        |> `Thm.concl_of
    1.98        |>> Logic.dest_equals