--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat May 30 23:30:54 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat May 30 23:58:06 2015 +0200
@@ -1934,10 +1934,10 @@
(rtac @{thm polarise} 1 THEN atac 1)
ORELSE
(REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
- THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
+ THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1))
- THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
+ THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
THEN
(HEADGOAL atac
ORELSE
@@ -2160,7 +2160,7 @@
| "replace_andrewsEQ" => nonfull_extcnf_combined_tac [Assumption]
| "split_preprocessing" =>
(REPEAT (HEADGOAL (split_simp_tac ctxt)))
- THEN TRY (PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion))
+ THEN TRY (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion))
THEN HEADGOAL atac
(*FIXME some of these could eventually be handled specially*)