# HG changeset patch
# User paulson
# Date 847101375 -3600
# Node ID 77dfe65b5bb347bc26b908916430139f6d455e51
# Parent  50c26585e5231f7c8aeebd67434bbc70a7e24239
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes

diff -r 50c26585e523 -r 77dfe65b5bb3 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Nov 04 10:54:26 1996 +0100
+++ b/src/Pure/tctical.ML	Mon Nov 04 10:56:15 1996 +0100
@@ -331,7 +331,7 @@
   Vars then it returns ct==>ct.*)
 fun eq_trivial ct =
   let val xfree = cterm_of Sign.proto_pure (Free (gensym"X", propT))
-      val ct_eq_x = mk_prop_equals (adjust_maxidx ct, xfree)
+      val ct_eq_x = mk_prop_equals (ct, xfree)
       and refl_ct = reflexive ct
       fun restore th = 
 	  implies_elim 
@@ -347,15 +347,16 @@
 (*Does the work of SELECT_GOAL. *)
 fun select tac st0 i =
   let val cprem::_ = drop(i-1, cprems_of st0)
-      val (eq_cprem, restore) = eq_trivial cprem
+      val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
+	                        eq_trivial (adjust_maxidx cprem)
       fun next st = bicompose false (false, restore st, nprems_of st) i st0
   in  Sequence.flats (Sequence.maps next (tac eq_cprem))
   end;
 
-(* (!!x. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
+(* (!!selct. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
 val dummy_quant_rl = 
-  standard (forall_elim_var 0 (assume 
-                  (read_cterm Sign.proto_pure ("!!x::prop. PROP V",propT))));
+  read_cterm Sign.proto_pure ("!!selct::prop. PROP V",propT) |>
+  assume |> forall_elim_var 0 |> standard;
 
 (* Prevent the subgoal's assumptions from becoming additional subgoals in the
    new proof state by enclosing them by a universal quantification *)