diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Thu Mar 02 12:07:20 1995 +0100
+++ b/src/Pure/tctical.ML	Fri Mar 03 11:48:05 1995 +0100
@@ -437,7 +437,7 @@
 (* (!!x. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
 val dummy_quant_rl = 
   standard (forall_elim_var 0 (assume 
-                  (read_cterm Sign.pure ("!!x::prop. PROP V",propT))));
+                  (read_cterm Sign.proto_pure ("!!x::prop. PROP V",propT))));
 
 (* Prevent the subgoal's assumptions from becoming additional subgoals in the
    new proof state by enclosing them by a universal quantification *)