--- a/Nominal/nominal_thmdecls.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_thmdecls.ML Tue Mar 22 12:18:30 2016 +0000
@@ -183,8 +183,9 @@
in
REPEAT o FIRST'
[CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms),
- rtac (thm RS @{thm "trans"}),
- rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}]
+ resolve_tac ctxt [thm RS @{thm trans}],
+ resolve_tac ctxt @{thms trans[OF "permute_fun_def"]} THEN'
+ resolve_tac ctxt @{thms ext}]
end
in
@@ -213,8 +214,12 @@
let
val ss_thms = @{thms "permute_minus_cancel"(2)}
in
- EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt,
- rtac @{thm "permute_boolI"}, dtac thm',
+ EVERY' [resolve_tac ctxt @{thms iffI},
+ dresolve_tac ctxt @{thms permute_boolE},
+ resolve_tac ctxt [thm],
+ assume_tac ctxt,
+ resolve_tac ctxt @{thms permute_boolI},
+ dresolve_tac ctxt [thm'],
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
end
@@ -232,7 +237,7 @@
val p = concl |> dest_comb |> snd |> find_perm
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
- val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm
+ val thm' = infer_instantiate ctxt' [(#1 (dest_Var p), Thm.cterm_of ctxt' (mk_minus p'))] thm
in
Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1)
|> singleton (Proof_Context.export ctxt' ctxt)