# HG changeset patch
# User lcp
# Date 749900013 -3600
# Node ID eb01df4ffe66191c9c673fbe776657f1d02d69ee
# Parent  d49df4181f0d85d31862089972999bdf74282563
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
?'a from occurring -- which sometimes caused SELECT_GOAL to fail

diff -r d49df4181f0d -r eb01df4ffe66 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Oct 06 09:58:53 1993 +0100
+++ b/src/Pure/tctical.ML	Wed Oct 06 10:33:33 1993 +0100
@@ -395,18 +395,17 @@
   The "main goal" of the new state will not be atomic, some tactics may fail!
   DOES NOT work if tactic affects the main goal other than by instantiation.*)
 
-(* (!!x. ?V) ==> ?V ;  used by protect_subgoal.*)
+(* (!!x. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
 val dummy_quant_rl = 
   standard (forall_elim_var 0 (assume 
-                  (Sign.read_cterm Sign.pure ("!!x. PROP V",propT))));
+                  (Sign.read_cterm Sign.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 =
-  case Sequence.chop (1, bicompose false (false,dummy_quant_rl,1) i state)
-  of
+  case Sequence.chop (1, bicompose false (false,dummy_quant_rl,1) i state) of
       ([state'],_) => state'
-    | _ => error"SELECT_GOAL -- impossible error???";
+    | _            => error"SELECT_GOAL -- impossible error???";
 
 (*Does the work of SELECT_GOAL. *)
 fun select (Tactic tf) state i =
@@ -416,16 +415,14 @@
   in  Sequence.flats (Sequence.maps next (tf st0))
   end;
 
-(*If i=1 and there is only one subgoal then do nothing!*)
 fun SELECT_GOAL tac i = Tactic (fn state =>
   case (i, drop(i-1, prems_of state)) of
       (_,[]) => Sequence.null
-    | (1,[_]) => tapply(tac,state)
+    | (1,[_]) => tapply(tac,state)  (*If i=1 and only one subgoal do nothing!*)
     | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal state i) i
     | (_, _::_) => select tac state i);
 
 
-
 (*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
     H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters. 
   Main difference from strip_assums concerns parameters: