src/Tools/misc_legacy.ML
changeset 60358 aebfbcab1eb8
parent 59621 291934bac95e
child 60642 48dd1cefb4ae
     1.1 --- a/src/Tools/misc_legacy.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/Tools/misc_legacy.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4    val mk_defpair: term * term -> string * term
     1.5    val get_def: theory -> xstring -> thm
     1.6    val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic
     1.7 -  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
     1.8 -  val freeze_thaw: thm -> thm * (thm -> thm)
     1.9 +  val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm)
    1.10 +  val freeze_thaw: Proof.context -> thm -> thm * (thm -> thm)
    1.11  end;
    1.12  
    1.13  structure Misc_Legacy: MISC_LEGACY =
    1.14 @@ -161,13 +161,12 @@
    1.15  fun metahyps_aux_tac ctxt tacf (prem,gno) state =
    1.16    let val (insts,params,hyps,concl) = metahyps_split_prem prem
    1.17        val maxidx = Thm.maxidx_of state
    1.18 -      val cterm = Thm.global_cterm_of (Thm.theory_of_thm state)
    1.19 -      val chyps = map cterm hyps
    1.20 +      val chyps = map (Thm.cterm_of ctxt) hyps
    1.21        val hypths = map Thm.assume chyps
    1.22        val subprems = map (Thm.forall_elim_vars 0) hypths
    1.23        val fparams = map Free params
    1.24 -      val cparams = map cterm fparams
    1.25 -      fun swap_ctpair (t,u) = (cterm u, cterm t)
    1.26 +      val cparams = map (Thm.cterm_of ctxt) fparams
    1.27 +      fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t)
    1.28        (*Subgoal variables: make Free; lift type over params*)
    1.29        fun mk_subgoal_inst concl_vars (v, T) =
    1.30            if member (op =) concl_vars (v, T)
    1.31 @@ -175,12 +174,12 @@
    1.32            else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
    1.33        (*Instantiate subgoal vars by Free applied to params*)
    1.34        fun mk_ctpair (v, in_concl, u) =
    1.35 -          if in_concl then (cterm (Var v), cterm u)
    1.36 -          else (cterm (Var v), cterm (list_comb (u, fparams)))
    1.37 +          if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u)
    1.38 +          else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams))
    1.39        (*Restore Vars with higher type and index*)
    1.40        fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
    1.41 -          if in_concl then (cterm u, cterm (Var ((a, i), T)))
    1.42 -          else (cterm u, cterm (Var ((a, i + maxidx), U)))
    1.43 +          if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T))
    1.44 +          else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U))
    1.45        (*Embed B in the original context of params and hyps*)
    1.46        fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
    1.47        (*Strip the context using elimination rules*)
    1.48 @@ -193,7 +192,7 @@
    1.49              and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
    1.50              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
    1.51              val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
    1.52 -            val emBs = map (cterm o embed) (Thm.prems_of st')
    1.53 +            val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
    1.54              val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
    1.55          in  (*restore the unknowns to the hypotheses*)
    1.56              free_instantiate (map swap_ctpair insts @
    1.57 @@ -206,7 +205,7 @@
    1.58        fun next st =
    1.59          Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
    1.60            (false, relift st, Thm.nprems_of st) gno state
    1.61 -  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
    1.62 +  in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end;
    1.63  
    1.64  fun print_vars_terms ctxt n thm =
    1.65    let
    1.66 @@ -255,9 +254,8 @@
    1.67  (*Convert all Vars in a theorem to Frees.  Also return a function for
    1.68    reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
    1.69  
    1.70 -fun freeze_thaw_robust th =
    1.71 +fun freeze_thaw_robust ctxt th =
    1.72   let val fth = Thm.legacy_freezeT th
    1.73 -     val thy = Thm.theory_of_thm fth
    1.74   in
    1.75     case Thm.fold_terms Term.add_vars fth [] of
    1.76         [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
    1.77 @@ -265,8 +263,8 @@
    1.78           let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
    1.79               val alist = map newName vars
    1.80               fun mk_inst (v,T) =
    1.81 -                 (Thm.global_cterm_of thy (Var(v,T)),
    1.82 -                  Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
    1.83 +                 apply2 (Thm.cterm_of ctxt)
    1.84 +                  (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
    1.85               val insts = map mk_inst vars
    1.86               fun thaw i th' = (*i is non-negative increment for Var indexes*)
    1.87                   th' |> forall_intr_list (map #2 insts)
    1.88 @@ -276,9 +274,8 @@
    1.89  
    1.90  (*Basic version of the function above. No option to rename Vars apart in thaw.
    1.91    The Frees created from Vars have nice names.*)
    1.92 -fun freeze_thaw th =
    1.93 +fun freeze_thaw ctxt th =
    1.94   let val fth = Thm.legacy_freezeT th
    1.95 -     val thy = Thm.theory_of_thm fth
    1.96   in
    1.97     case Thm.fold_terms Term.add_vars fth [] of
    1.98         [] => (fth, fn x => x)
    1.99 @@ -289,8 +286,7 @@
   1.100               val (alist, _) =
   1.101                   fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
   1.102               fun mk_inst (v, T) =
   1.103 -                 (Thm.global_cterm_of thy (Var(v,T)),
   1.104 -                  Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   1.105 +                apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
   1.106               val insts = map mk_inst vars
   1.107               fun thaw th' =
   1.108                   th' |> forall_intr_list (map #2 insts)
   1.109 @@ -299,4 +295,3 @@
   1.110   end;
   1.111  
   1.112  end;
   1.113 -