# HG changeset patch
# User wenzelm
# Date 911308045 -3600
# Node ID 1f58694fc3e227c594eaa4c6c271804a69fb6c68
# Parent  68cdba6c178fc40e8fc8da65c49a07ad3e38ef33
Drule.rev_triv_goal;

diff -r 68cdba6c178f -r 1f58694fc3e2 src/Pure/tctical.ML
--- 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))