# HG changeset patch # User wenzelm # Date 1425558484 -3600 # Node ID eb59c6968219fbdcd573c9d5e1021812ba4daf49 # Parent 304ee0a475d193f3d68ff14192fbabe3111bf116 tuned -- more explicit use of context; diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Isar/element.ML Thu Mar 05 13:28:04 2015 +0100 @@ -201,9 +201,9 @@ (case Object_Logic.elim_concl th of SOME C => let - val cert = Thm.cterm_of (Thm.theory_of_thm th); + val thy = Thm.theory_of_thm th; val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); - val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th; + val th' = Thm.instantiate ([], [(Thm.cterm_of thy C, Thm.cterm_of thy thesis)]) th; in (th', true) end | NONE => (th, false)); @@ -338,9 +338,8 @@ fun instantiate_tfrees thy subst th = let - val certT = Thm.ctyp_of thy; val idx = Thm.maxidx_of th + 1; - fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T); + fun cert_inst (a, (S, T)) = (Thm.ctyp_of thy (TVar ((a, idx), S)), Thm.ctyp_of thy T); fun add_inst (a, S) insts = if AList.defined (op =) insts a then insts @@ -355,10 +354,8 @@ end; fun instantiate_frees thy subst = - let val cert = Thm.cterm_of thy in - Drule.forall_intr_list (map (cert o Free o fst) subst) #> - Drule.forall_elim_list (map (cert o snd) subst) - end; + Drule.forall_intr_list (map (Thm.cterm_of thy o Free o fst) subst) #> + Drule.forall_elim_list (map (Thm.cterm_of thy o snd) subst); fun hyps_rule rule th = let val {hyps, ...} = Thm.crep_thm th in diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Isar/expression.ML Thu Mar 05 13:28:04 2015 +0100 @@ -678,18 +678,17 @@ [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])]; val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head; - val cert = Thm.cterm_of defs_thy; - val intro = Goal.prove_global defs_thy [] norm_ts statement (fn {context = ctxt, ...} => rewrite_goals_tac ctxt [pred_def] THEN compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt - (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); + (false, + Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF - [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))]) + [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))]) |> Conjunction.elim_balanced (length ts); val (_, axioms_ctxt) = defs_ctxt diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Isar/generic_target.ML Thu Mar 05 13:28:04 2015 +0100 @@ -176,11 +176,10 @@ fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = let - val thy = Proof_Context.theory_of lthy; - val thy_ctxt = Proof_Context.init_global thy; + val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (*term and type parameters*) - val ((defs, _), rhs') = Thm.cterm_of thy rhs + val ((defs, _), rhs') = Proof_Context.cterm_of lthy rhs |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; val xs = Variable.add_fixed lthy rhs' []; @@ -218,10 +217,7 @@ fun import_export_proof ctxt (name, raw_th) = let - val thy = Proof_Context.theory_of ctxt; - val thy_ctxt = Proof_Context.init_global thy; - val certT = Thm.ctyp_of thy; - val cert = Thm.cterm_of thy; + val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt); (*export assumes/defines*) val th = Goal.norm_result ctxt raw_th; @@ -232,7 +228,7 @@ val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); val frees = map Free (Thm.fold_terms Term.add_frees th' []); val (th'' :: vs) = - (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) + (th' :: map (Drule.mk_term o Proof_Context.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |> Variable.export ctxt thy_ctxt |> Drule.zero_var_indexes_list; @@ -246,8 +242,10 @@ val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); val inst = filter (is_Var o fst) (vars ~~ frees); - val cinstT = map (apply2 certT o apfst TVar) instT; - val cinst = map (apply2 (cert o Term.map_types (Term_Subst.instantiateT instT))) inst; + val cinstT = instT + |> map (apply2 (Proof_Context.ctyp_of ctxt) o apfst TVar); + val cinst = inst + |> map (apply2 (Proof_Context.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT))); val result' = Thm.instantiate (cinstT, cinst) result; (*import assumes/defines*) diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Isar/obtain.ML Thu Mar 05 13:28:04 2015 +0100 @@ -112,8 +112,6 @@ name raw_vars raw_asms int state = let val _ = Proof.assert_forward_or_chain state; - val thy = Proof.theory_of state; - val cert = Thm.cterm_of thy; val ctxt = Proof.context_of state; val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; @@ -131,6 +129,7 @@ (*obtain parms*) val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt; val parms = map Free (xs' ~~ Ts); + val cparms = map (Proof_Context.cterm_of ctxt) parms; val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt; (*obtain statements*) @@ -149,7 +148,7 @@ Proof.local_qed (NONE, false) #> `Proof.the_fact #-> (fn rule => Proof.fix vars - #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms); + #> Proof.assm (obtain_export fix_ctxt rule cparms) asms); in state |> Proof.enter_forward @@ -187,18 +186,18 @@ fun result tac facts ctxt = let - val cert = Proof_Context.cterm_of ctxt; - val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN; + val st = Goal.init (Proof_Context.cterm_of ctxt thesis); val rule = - (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of + (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of NONE => raise THM ("Obtain.result: tactic failed", 0, facts) | SOME th => check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th))); - val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule; + val closed_rule = Thm.forall_intr (Proof_Context.cterm_of ctxt (Free thesis_var)) rule; val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; - val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule'; + val obtain_rule = + Thm.forall_elim (Proof_Context.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule'; val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt'; val (prems, ctxt'') = Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) @@ -214,8 +213,6 @@ fun unify_params vars thesis_var raw_rule ctxt = let val thy = Proof_Context.theory_of ctxt; - val certT = Thm.ctyp_of thy; - val cert = Thm.cterm_of thy; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th); @@ -240,20 +237,20 @@ val xs = map (apsnd norm_type o fst) vars; val ys = map (apsnd norm_type) (drop m params); val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; - val terms = map (Drule.mk_term o cert o Free) (xs @ ys'); + val terms = map (Drule.mk_term o Thm.cterm_of thy o Free) (xs @ ys'); val instT = fold (Term.add_tvarsT o #2) params [] - |> map (TVar #> (fn T => (certT T, certT (norm_type T)))); + |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T)))); val closed_rule = rule - |> Thm.forall_intr (cert (Free thesis_var)) + |> Thm.forall_intr (Thm.cterm_of thy (Free thesis_var)) |> Thm.instantiate (instT, []); val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; val vars' = map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ (map snd vars @ replicate (length ys) NoSyn); - val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule'; + val rule'' = Thm.forall_elim (Thm.cterm_of thy (Logic.varify_global (Free thesis_var))) rule'; in ((vars', rule''), ctxt') end; fun inferred_type (binding, _, mx) ctxt = @@ -270,7 +267,6 @@ let val _ = Proof.assert_forward_or_chain state; val ctxt = Proof.context_of state; - val cert = Proof_Context.cterm_of ctxt; val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN); @@ -292,7 +288,8 @@ |> Proof.map_context (K ctxt') |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm - (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)]) + (obtain_export fix_ctxt rule (map (Proof_Context.cterm_of ctxt) ts)) + [(Thm.empty_binding, asms)]) |> Proof.bind_terms Auto_Bind.no_facts end; @@ -314,7 +311,8 @@ |> Proof.chain_facts chain_facts |> Proof.local_goal print_result (K I) (pair o rpair I) "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])] - |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (cert thesis))) |> Seq.hd + |> Proof.refine (Method.primitive_text (fn _ => fn _ => + Goal.init (Proof_Context.cterm_of ctxt thesis))) |> Seq.hd end; in diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Isar/proof.ML Thu Mar 05 13:28:04 2015 +0100 @@ -894,7 +894,6 @@ fun generic_goal prepp kind before_qed after_qed raw_propp state = let val ctxt = context_of state; - val cert = Proof_Context.cterm_of ctxt; val chaining = can assert_chain state; val pos = Position.thread_data (); @@ -910,7 +909,8 @@ val propss' = vars :: propss; val goal_propss = filter_out null propss'; val goal = - cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)) + Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss) + |> Proof_Context.cterm_of ctxt |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state)); val statement = ((kind, pos), propss', Thm.term_of goal); val after_qed' = after_qed |>> (fn after_local => diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 05 13:28:04 2015 +0100 @@ -1166,10 +1166,10 @@ fun gen_assms prepp exp args ctxt = let - val cert = cterm_of ctxt; val ((propss, _), ctxt1) = prepp (map snd args) ctxt; val _ = Variable.warn_extra_tfrees ctxt ctxt1; - val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1; + val (premss, ctxt2) = + fold_burrow (Assumption.add_assms exp o map (cterm_of ctxt)) propss ctxt1; in ctxt2 |> auto_bind_facts (flat propss) diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Thu Mar 05 13:28:04 2015 +0100 @@ -81,8 +81,6 @@ fun read_insts ctxt mixed_insts (tvars, vars) = let val thy = Proof_Context.theory_of ctxt; - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts; @@ -118,7 +116,8 @@ val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; val inst_vars = map_filter (make_inst inst2) vars2; in - (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars) + (map (apply2 (Thm.ctyp_of thy)) inst_tvars, + map (apply2 (Thm.cterm_of thy)) inst_vars) end; fun where_rule ctxt mixed_insts fixes thm = @@ -282,9 +281,9 @@ fun make_elim_preserve ctxt rl = let - val cert = Thm.cterm_of (Thm.theory_of_thm rl); + val thy = Thm.theory_of_thm rl; val maxidx = Thm.maxidx_of rl; - fun cvar xi = cert (Var (xi, propT)); + fun cvar xi = Thm.cterm_of thy (Var (xi, propT)); val revcut_rl' = Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)), (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl; diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/drule.ML Thu Mar 05 13:28:04 2015 +0100 @@ -210,10 +210,8 @@ (*generalize outermost parameters*) fun gen_all th = let - val thy = Thm.theory_of_thm th; - val {prop, maxidx, ...} = Thm.rep_thm th; - val cert = Thm.cterm_of thy; - fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T))); + val {thy, prop, maxidx, ...} = Thm.rep_thm th; + fun elim (x, T) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T))); in fold elim (outer_params prop) th end; (*lift vars wrt. outermost goal parameters @@ -221,16 +219,15 @@ fun lift_all goal th = let val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th); - val cert = Thm.cterm_of thy; val maxidx = Thm.maxidx_of th; val ps = outer_params (Thm.term_of goal) |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); val Ts = map Term.fastype_of ps; val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) => - (cert (Var (xi, T)), cert (Term.list_comb (Var (xi, Ts ---> T), ps)))); + (Thm.cterm_of thy (Var (xi, T)), Thm.cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps)))); in th |> Thm.instantiate ([], inst) - |> fold_rev (Thm.forall_intr o cert) ps + |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) ps end; (*direct generalization*) @@ -250,10 +247,9 @@ | zero_var_indexes_list ths = let val thy = Theory.merge_list (map Thm.theory_of_thm ths); - val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy; val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); - val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT; - val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst; + val cinstT = map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT; + val cinst = map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst; in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end; val zero_var_indexes = singleton zero_var_indexes_list; @@ -647,12 +643,10 @@ fun mk_term ct = let val thy = Thm.theory_of_cterm ct; - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; val T = Thm.typ_of_cterm ct; - val a = certT (TVar (("'a", 0), [])); - val x = cert (Var (("x", 0), T)); - in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end; + val a = Thm.ctyp_of thy (TVar (("'a", 0), [])); + val x = Thm.cterm_of thy (Var (("x", 0), T)); + in Thm.instantiate ([(a, Thm.ctyp_of thy T)], [(x, ct)]) termI end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in @@ -793,10 +787,9 @@ | cterm_instantiate ctpairs th = let val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); - val certT = Thm.ctyp_of thy; val instT = Vartab.fold (fn (xi, (S, T)) => - cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye []; + cons (Thm.ctyp_of thy (TVar (xi, S)), Thm.ctyp_of thy (Envir.norm_type tye T))) tye []; val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs; in instantiate_normalize (instT, inst) th end handle TERM (msg, _) => raise THM (msg, 0, [th]) @@ -846,18 +839,18 @@ fun rename_bvars [] thm = thm | rename_bvars vs thm = let - val cert = Thm.cterm_of (Thm.theory_of_thm thm); + val thy = Thm.theory_of_thm thm; fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t) | ren (t $ u) = ren t $ ren u | ren t = t; - in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end; + in Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy (ren (Thm.prop_of thm)))) thm end; (* renaming in left-to-right order *) fun rename_bvars' xs thm = let - val cert = Thm.cterm_of (Thm.theory_of_thm thm); + val thy = Thm.theory_of_thm thm; val prop = Thm.prop_of thm; fun rename [] t = ([], t) | rename (x' :: xs) (Abs (x, T, t)) = @@ -869,9 +862,10 @@ val (xs'', u') = rename xs' u in (xs'', t' $ u') end | rename xs t = (xs, t); - in case rename xs prop of - ([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm - | _ => error "More names than abstractions in theorem" + in + (case rename xs prop of + ([], prop') => Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy prop')) thm + | _ => error "More names than abstractions in theorem") end; end; diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/goal.ML Thu Mar 05 13:28:04 2015 +0100 @@ -128,20 +128,20 @@ fun future_result ctxt result prop = let val thy = Proof_Context.theory_of ctxt; - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; val assms = Assumption.all_assms_of ctxt; val As = map Thm.term_of assms; val xs = map Free (fold Term.add_frees (prop :: As) []); - val fixes = map cert xs; + val fixes = map (Thm.cterm_of thy) xs; val tfrees = fold Term.add_tfrees (prop :: As) []; - val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees; + val instT = + map (fn (a, S) => (Thm.ctyp_of thy (TVar ((a, 0), S)), Thm.ctyp_of thy (TFree (a, S)))) tfrees; val global_prop = - cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) + Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))) + |> Thm.cterm_of thy |> Thm.weaken_sorts (Variable.sorts_of ctxt); val global_result = result |> Future.map (Drule.flexflex_unique (SOME ctxt) #> diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/more_thm.ML Thu Mar 05 13:28:04 2015 +0100 @@ -116,18 +116,21 @@ fun add_cterm_frees ct = let - val cert = Thm.cterm_of (Thm.theory_of_cterm ct); + val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; - in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end; + in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.cterm_of thy v) | _ => I) t end; (* cterm constructors and destructors *) fun all_name (x, t) A = let - val cert = Thm.cterm_of (Thm.theory_of_cterm t); + val thy = Thm.theory_of_cterm t; val T = Thm.typ_of_cterm t; - in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end; + in + Thm.apply (Thm.cterm_of thy (Const ("Pure.all", (T --> propT) --> propT))) + (Thm.lambda_name (x, t) A) + end; fun all t A = all_name ("", t) A; diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/subgoal.ML --- a/src/Pure/subgoal.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/subgoal.ML Thu Mar 05 13:28:04 2015 +0100 @@ -67,7 +67,6 @@ *) fun lift_import idx params th ctxt = let - val cert = Proof_Context.cterm_of ctxt; val ((_, [th']), ctxt') = Variable.importT [th] ctxt; val Ts = map Thm.typ_of_cterm params; @@ -86,7 +85,8 @@ else (Ts ---> T, ts); val u = Free (y, U); in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; - val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys)); + val (inst1, inst2) = + split_list (map (apply2 (apply2 (Proof_Context.cterm_of ctxt))) (map2 var_inst vars ys)); val th'' = Thm.instantiate ([], inst1) th'; in ((inst2, th''), ctxt'') end; diff -r 304ee0a475d1 -r eb59c6968219 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Mar 05 11:11:42 2015 +0100 +++ b/src/Pure/variable.ML Thu Mar 05 13:28:04 2015 +0100 @@ -587,9 +587,9 @@ fun focus_cterm goal ctxt = let - val cert = Thm.cterm_of (Thm.theory_of_cterm goal); + val thy = Thm.theory_of_cterm goal; val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt; - val ps' = map (cert o Free) ps; + val ps' = map (Thm.cterm_of thy o Free) ps; val goal' = fold forall_elim_prop ps' goal; in ((xs ~~ ps', goal'), ctxt') end;