src/HOL/Tools/Function/function_context_tree.ML
changeset 59621 291934bac95e
parent 59618 e6939796717e
child 60695 757549b4bbe6
     1.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4          val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
     1.5          val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
     1.6          val inst =
     1.7 -          map (fn v => apply2 (Proof_Context.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
     1.8 +          map (fn v => apply2 (Thm.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
     1.9              (Term.add_vars c [])
    1.10        in
    1.11          (cterm_instantiate inst r, dep, branches)
    1.12 @@ -147,7 +147,7 @@
    1.13              val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t
    1.14              fun subtree (ctxt', fixes, assumes, st) =
    1.15                ((fixes,
    1.16 -                map (Thm.assume o Proof_Context.cterm_of ctxt) assumes),
    1.17 +                map (Thm.assume o Thm.cterm_of ctxt) assumes),
    1.18                 mk_tree' ctxt' st)
    1.19            in
    1.20              Cong (r, dep, map subtree branches)
    1.21 @@ -158,8 +158,8 @@
    1.22  
    1.23  fun inst_tree ctxt fvar f tr =
    1.24    let
    1.25 -    val cfvar = Proof_Context.cterm_of ctxt fvar
    1.26 -    val cf = Proof_Context.cterm_of ctxt f
    1.27 +    val cfvar = Thm.cterm_of ctxt fvar
    1.28 +    val cf = Thm.cterm_of ctxt f
    1.29  
    1.30      fun inst_term t =
    1.31        subst_bound(f, abstract_over (fvar, t))
    1.32 @@ -172,7 +172,7 @@
    1.33        | inst_tree_aux (RCall (t, str)) =
    1.34          RCall (inst_term t, inst_tree_aux str)
    1.35      and inst_branch ((fxs, assms), str) =
    1.36 -      ((fxs, map (Thm.assume o Proof_Context.cterm_of ctxt o inst_term o Thm.prop_of) assms),
    1.37 +      ((fxs, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) assms),
    1.38         inst_tree_aux str)
    1.39    in
    1.40      inst_tree_aux tr
    1.41 @@ -188,10 +188,10 @@
    1.42  
    1.43  fun export_thm ctxt (fixes, assumes) =
    1.44   fold_rev (Thm.implies_intr o Thm.cprop_of) assumes
    1.45 - #> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) fixes
    1.46 + #> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) fixes
    1.47  
    1.48  fun import_thm ctxt (fixes, athms) =
    1.49 - fold (Thm.forall_elim o Proof_Context.cterm_of ctxt o Free) fixes
    1.50 + fold (Thm.forall_elim o Thm.cterm_of ctxt o Free) fixes
    1.51   #> fold Thm.elim_implies athms
    1.52  
    1.53  
    1.54 @@ -240,7 +240,7 @@
    1.55  
    1.56  fun rewrite_by_tree ctxt h ih x tr =
    1.57    let
    1.58 -    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Proof_Context.cterm_of ctxt t), x)
    1.59 +    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Thm.cterm_of ctxt t), x)
    1.60        | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
    1.61          let
    1.62            val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
    1.63 @@ -248,10 +248,10 @@
    1.64            val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
    1.65              |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
    1.66                                                      (* (a, h a) : G   *)
    1.67 -          val inst_ih = instantiate' [] [SOME (Proof_Context.cterm_of ctxt arg)] ih
    1.68 +          val inst_ih = instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
    1.69            val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
    1.70  
    1.71 -          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Proof_Context.cterm_of ctxt h)) inner
    1.72 +          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of ctxt h)) inner
    1.73            val h_a_eq_f_a = eq RS eq_reflection
    1.74            val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
    1.75          in