src/Pure/tctical.ML

   DOES NOT work if tactic affects the main goal other than by instantiation.*)
 
 (* (!!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 *)
 fun protect_subgoal state i =
 	Sequence.hd (bicompose false (false,dummy_quant_rl,1) i state)