--- a/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 13:39:34 2015 +0100
@@ -80,7 +80,6 @@
fun mk_partial_elim_rules ctxt result =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
val n_fs = length fs;
@@ -116,12 +115,12 @@
val args = HOLogic.mk_tuple arg_vars;
val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
- val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
+ val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
- val cprop = cert prop;
+ val cprop = Proof_Context.cterm_of ctxt prop;
- val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+ val asms = [cprop, Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
val asms_thms = map Thm.assume asms;
fun prep_subgoal_tac i =
@@ -134,10 +133,10 @@
val elim_stripped =
nth cases idx
|> Thm.forall_elim P
- |> Thm.forall_elim (cert args)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt args)
|> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
|> fold_rev Thm.implies_intr asms
- |> Thm.forall_intr (cert rhs_var);
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt rhs_var);
val bool_elims =
(case ranT of
@@ -146,7 +145,7 @@
fun unstrip rl =
rl
- |> fold_rev (Thm.forall_intr o cert) arg_vars
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) arg_vars
|> Thm.forall_intr P
in
map unstrip (elim_stripped :: bool_elims)