# HG changeset patch
# User paulson
# Date 903023090 -7200
# Node ID b380921982b9595d5b6eb5de16969794b055fb5b
# Parent  f3f71669878e7fcb659a80e03a125364b77300eb
simpler SELECT_GOAL no longer inserts a dummy parameter

diff -r f3f71669878e -r b380921982b9 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Thu Aug 13 17:43:00 1998 +0200
+++ b/src/Pure/tctical.ML	Thu Aug 13 17:44:50 1998 +0200
@@ -363,8 +363,10 @@
 (*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible.
   It is paired with a function to undo the transformation.  If ct contains
   Vars then it returns ct==>ct.*)
+
 fun eq_trivial ct =
-  let val xfree = cterm_of (sign_of ProtoPure.thy) (Free (gensym"EQ_TRIVIAL_", propT))
+  let val xfree = cterm_of (sign_of ProtoPure.thy)
+                           (Free (gensym"EQ_TRIVIAL_", propT))
       val ct_eq_x = mk_prop_equals (ct, xfree)
       and refl_ct = reflexive ct
       fun restore th = 
@@ -373,36 +375,35 @@
             refl_ct
   in  (equal_elim
          (combination (combination refl_implies refl_ct) (assume ct_eq_x))
-         (trivial ct),
+         (Drule.mk_triv_goal ct),
        restore)
   end  (*Fails if there are Vars or TVars*)
-    handle THM _ => (trivial ct, I);
+    handle THM _ => (Drule.mk_triv_goal ct, I);
+
 
 (*Does the work of SELECT_GOAL. *)
-fun select tac st0 i =
+fun select tac st i =
   let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
-	  eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
-      fun next st = bicompose false (false, restore st, nprems_of st) i st0
+	  eq_trivial (adjust_maxidx (List.nth(cprems_of st, i-1)))
+      fun next st' = 
+	  let val np' = nprems_of st'
+              (*rename the ?A in rev_triv_goal*)
+	      val {maxidx,...} = rep_thm st'
+              val ct = cterm_of (sign_of ProtoPure.thy)
+		                (Var(("A",maxidx+1), propT))
+	      val rev_triv_goal' = instantiate' [] [Some ct] rev_triv_goal
+              fun bic th = bicompose false (false, th, np')
+          in  bic (Seq.hd (bic (restore st') 1 rev_triv_goal')) i st  end 
   in  Seq.flat (Seq.map next (tac eq_cprem))
   end;
 
-(* (!!selct. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
-val dummy_quant_rl = 
-  read_cterm (sign_of ProtoPure.thy) ("!!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 *)
-fun protect_subgoal st i =
-        Seq.hd (bicompose false (false,dummy_quant_rl,1) i st)
-        handle _ => error"SELECT_GOAL -- impossible error???";
-
 fun SELECT_GOAL tac i st = 
-  case (i, List.drop(prems_of st, i-1)) of
-      (_,[]) => Seq.empty
-    | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
-    | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
-    | (_, _::_) => select tac st i;
+  let val np = nprems_of st
+  in  if 1<=i andalso i<=np then 
+          (*If only one subgoal, then just apply tactic*)
+	  if np=1 then tac st else select tac st i
+      else Seq.empty
+  end;
 
 
 (*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )