src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Thu Mar 02 12:07:20 1995 +0100
+++ b/src/Pure/tactic.ML	Fri Mar 03 11:48:05 1995 +0100
@@ -238,7 +238,7 @@
   increment revcut_rl instead.*)
 fun make_elim_preserve rl = 
   let val {maxidx,...} = rep_thm rl
-      fun cvar ixn = cterm_of Sign.pure (Var(ixn,propT));
+      fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
       val revcut_rl' = 
 	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
 			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl