--- a/src/Pure/tctical.ML Tue Nov 17 14:07:04 1998 +0100
+++ b/src/Pure/tctical.ML Tue Nov 17 14:07:25 1998 +0100
@@ -391,7 +391,7 @@
val {maxidx,...} = rep_thm st'
val ct = cterm_of (sign_of ProtoPure.thy)
(Var(("A",maxidx+1), propT))
- val rev_triv_goal' = instantiate' [] [Some ct] rev_triv_goal
+ val rev_triv_goal' = instantiate' [] [Some ct] Drule.rev_triv_goal
fun bic th = bicompose false (false, th, np')
in bic (Seq.hd (bic (restore st') 1 rev_triv_goal')) i st end
in Seq.flat (Seq.map next (tac eq_cprem))