--- a/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 11:03:02 2015 +0200
@@ -591,7 +591,7 @@
val monos = Inductive.get_monos ctxt;
val intrs' = Inductive.unpartition_rules intrs
(map (fn (((s, ths), (_, k)), th) =>
- (s, ths ~~ Inductive.infer_intro_vars th k ths))
+ (s, ths ~~ Inductive.infer_intro_vars thy th k ths))
(Inductive.partition_rules raw_induct intrs ~~
Inductive.arities_of raw_induct ~~ elims));
val k = length (Inductive.params_of raw_induct);
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 02 11:03:02 2015 +0200
@@ -1449,7 +1449,7 @@
(the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
- |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
+ |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
@{thms eqTrueE eq_False[THEN iffD1] notnotD}
|> pair eqn_pos
|> single
--- a/src/HOL/Tools/Meson/meson.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Tue Jun 02 11:03:02 2015 +0200
@@ -11,7 +11,7 @@
val trace : bool Config.T
val max_clauses : int Config.T
val term_pair_of: indexname * (typ * 'a) -> term * 'a
- val first_order_resolve : thm -> thm -> thm
+ val first_order_resolve : Proof.context -> thm -> thm -> thm
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
@@ -98,16 +98,16 @@
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
(*FIXME: currently does not "rename variables apart"*)
-fun first_order_resolve thA thB =
+fun first_order_resolve ctxt thA thB =
(case
try (fn () =>
- let val thy = Thm.theory_of_thm thA
+ let val thy = Proof_Context.theory_of ctxt
val tmA = Thm.concl_of thA
val Const(@{const_name Pure.imp},_) $ tmB $ _ = Thm.prop_of thB
val tenv =
Pattern.first_order_match thy (tmB, tmA)
(Vartab.empty, Vartab.empty) |> snd
- val ct_pairs = map (apply2 (Thm.global_cterm_of thy) o term_pair_of) (Vartab.dest tenv)
+ val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
in thA RS (cterm_instantiate ct_pairs thB) end) () of
SOME th => th
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
@@ -359,11 +359,10 @@
in (th RS spec', ctxt') end
end;
-fun apply_skolem_theorem (th, rls) =
+fun apply_skolem_theorem ctxt (th, rls) =
let
fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
- | tryall (rl :: rls) =
- first_order_resolve th rl handle THM _ => tryall rls
+ | tryall (rl :: rls) = first_order_resolve ctxt th rl handle THM _ => tryall rls
in tryall rls end
(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
@@ -383,7 +382,7 @@
in ctxt_ref := ctxt'; cnf_aux (th', ths) end
| Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
- cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
+ cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths)
| Const (@{const_name HOL.disj}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Jun 02 11:03:02 2015 +0200
@@ -85,7 +85,7 @@
(case add_vars_and_frees u [] of
[] =>
Conv.abs_conv (conv false o snd) ctxt ct
- |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
+ |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI})
| v :: _ =>
Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
|> Thm.cterm_of ctxt
--- a/src/HOL/Tools/choice_specification.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Tue Jun 02 11:03:02 2015 +0200
@@ -140,7 +140,7 @@
val cT = Thm.ctyp_of_cterm cv
val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
in thm RS spec' end
- fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm
+ fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
fun process_single ((name, atts), rew_imp, frees) args =
let
fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm
@@ -152,7 +152,7 @@
Global_Theory.store_thm (Binding.name name, thm) thy)
in
swap args
- |> apfst (remove_alls frees)
+ |> remove_alls frees
|> apfst undo_imps
|> apfst Drule.export_without_context
|-> Thm.theory_attributes
--- a/src/HOL/Tools/inductive.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Jun 02 11:03:02 2015 +0200
@@ -65,7 +65,7 @@
val partition_rules: thm -> thm list -> (string * thm list) list
val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
- val infer_intro_vars: thm -> int -> thm list -> term list list
+ val infer_intro_vars: theory -> thm -> int -> thm list -> term list list
end;
signature INDUCTIVE =
@@ -1132,9 +1132,8 @@
(fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
(* infer order of variables in intro rules from order of quantifiers in elim rule *)
-fun infer_intro_vars elim arity intros =
+fun infer_intro_vars thy elim arity intros =
let
- val thy = Thm.theory_of_thm elim;
val _ :: cases = Thm.prems_of elim;
val used = map (fst o fst) (Term.add_vars (Thm.prop_of elim) []);
fun mtch (t, u) =
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 02 11:03:02 2015 +0200
@@ -19,9 +19,9 @@
[name] => name
| _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
-fun prf_of thm =
+fun prf_of thy thm =
Reconstruct.proof_of thm
- |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *)
+ |> Reconstruct.expand_proof thy [("", NONE)]; (* FIXME *)
fun subsets [] = [[]]
| subsets (x::xs) =
@@ -268,7 +268,7 @@
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
Extraction.abs_corr_shyps thy rule vs vs2
(ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
- (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
+ (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
end;
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
@@ -285,7 +285,7 @@
val params' = map dest_Var params;
val rss = Inductive.partition_rules raw_induct intrs;
val rss' = map (fn (((s, rs), (_, arity)), elim) =>
- (s, (Inductive.infer_intro_vars elim arity rs ~~ rs)))
+ (s, (Inductive.infer_intro_vars thy elim arity rs ~~ rs)))
(rss ~~ arities ~~ elims);
val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
--- a/src/HOL/Tools/split_rule.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/split_rule.ML Tue Jun 02 11:03:02 2015 +0200
@@ -39,12 +39,11 @@
| ap_split _ T3 u = u;
(*Curries any Var of function type in the rule*)
-fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
+fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
let val T' = HOLogic.flatten_tupleT T1 ---> T2;
val newt = ap_split T1 T2 (Var (v, T'));
- val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
- in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
- | split_rule_var' _ rl = rl;
+ in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end
+ | split_rule_var' _ _ rl = rl;
(* complete splitting of partially split rules *)
@@ -85,11 +84,11 @@
fun split_rule_var ctxt =
- (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var';
+ (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt;
(*curries ALL function variables occurring in a rule's conclusion*)
fun split_rule ctxt rl =
- fold_rev split_rule_var' (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
+ fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
|> remove_internal_split ctxt
|> Drule.export_without_context;
--- a/src/Provers/splitter.ML Tue Jun 02 10:12:46 2015 +0200
+++ b/src/Provers/splitter.ML Tue Jun 02 11:03:02 2015 +0200
@@ -285,9 +285,8 @@
call split_posns with appropriate parameters
*************************************************************)
-fun select cmap state i =
+fun select thy cmap state i =
let
- val thy = Thm.theory_of_thm state
val goal = Thm.term_of (Thm.cprem_of state i);
val Ts = rev (map #2 (Logic.strip_params goal));
val _ $ t $ _ = Logic.strip_assums_concl goal;
@@ -313,16 +312,14 @@
i : no. of subgoal
**************************************************************)
-fun inst_lift Ts t (T, U, pos) state i =
+fun inst_lift ctxt Ts t (T, U, pos) state i =
let
- val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
val (cntxt, u) = mk_cntxt t pos (T --> U);
val trlift' = Thm.lift_rule (Thm.cprem_of state i)
(Thm.rename_boundvars abs_lift u trlift);
val (P, _) = strip_comb (fst (Logic.dest_equals
(Logic.strip_assums_concl (Thm.prop_of trlift'))));
- in cterm_instantiate [(cert P, cert (abss Ts cntxt))] trlift'
- end;
+ in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end;
(*************************************************************
@@ -338,15 +335,13 @@
i : number of subgoal
**************************************************************)
-fun inst_split Ts t tt thm TB state i =
+fun inst_split ctxt Ts t tt thm TB state i =
let
val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
val (P, _) = strip_comb (fst (Logic.dest_equals
(Logic.strip_assums_concl (Thm.prop_of thm'))));
- val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
val cntxt = mk_cntxt_splitthm t tt TB;
- in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
- end;
+ in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end;
(*****************************************************************************
@@ -359,14 +354,15 @@
fun split_tac _ [] i = no_tac
| split_tac ctxt splits i =
let val cmap = cmap_of_split_thms splits
- fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st
+ fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift ctxt Ts t p st i, 2) i st
fun lift_split_tac state =
- let val (Ts, t, splits) = select cmap state i
+ let val (Ts, t, splits) = select (Proof_Context.theory_of ctxt) cmap state i
in case splits of
[] => no_tac state
| (thm, apsns, pos, TB, tt)::_ =>
(case apsns of
- [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state
+ [] =>
+ compose_tac ctxt (false, inst_split ctxt Ts t tt thm TB state i, 0) i state
| p::_ => EVERY [lift_tac Ts t p,
resolve_tac ctxt [reflexive_thm] (i+1),
lift_split_tac] state)