--- 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 *)