Removal of the tactical STATE

--- a/src/CCL/typecheck.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/CCL/typecheck.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -83,9 +83,8 @@
                  could_unify(x,hd (prems_of rcall2T)) orelse
                  could_unify(x,hd (prems_of rcall3T));
 
-fun IHinst tac rls i = STATE (fn state =>
-  let val (_,_,Bi,_) = dest_state(state,i);
-      val bvs = bvars Bi [];
+fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
+  let val bvs = bvars Bi [];
       val ihs = filter could_IH (Logic.strip_assums_hyp Bi);
       val rnames = map (fn x=>
                     let val (a,b) = get_bno [] 0 x
@@ -113,12 +112,8 @@
                            ematch_tac [SubtypeE] i ORELSE
                            match_tac [SubtypeI] i;
 
-fun tc_step_tac prems i = STATE(fn state =>
-          if (i>length(prems_of state)) 
-             then no_tac
-             else let val (_,_,c,_) = dest_state(state,i)
-                  in if is_rigid_prog c then raw_step_tac prems i else no_tac
-                  end);
+fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
+          if is_rigid_prog Bi then raw_step_tac prems i else no_tac);
 
 fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i;
 

--- a/src/FOL/simpdata.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/FOL/simpdata.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -257,18 +257,21 @@
 
 (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    fails if there is no equaliy or if an equality is already at the front *)
-fun rot_eq_tac i = let
+local
   fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
-  |   is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
-  |   is_eq _ = false;
+    | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
+    | is_eq _ = false;
   fun find_eq n [] = None
-  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
-  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
-	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
-	      None   => no_tac
-	    | Some 0 => no_tac
-	    | Some n => rotate_tac n i) end;
-in STATE rot_eq end;
+    | find_eq n (t :: ts) = if (is_eq t) then Some n 
+			    else find_eq (n + 1) ts;
+in
+val rot_eq_tac = 
+     SUBGOAL (fn (Bi,i) => 
+	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
+		  None   => no_tac
+		| Some 0 => no_tac
+		| Some n => rotate_tac n i)
+end;
 
 
 fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 

--- a/src/FOLP/hypsubst.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/FOLP/hypsubst.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -67,18 +67,18 @@
 
 (*Select a suitable equality assumption and substitute throughout the subgoal
   Replaces only Bound variables if bnd is true*)
-fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
-      let val (_,_,Bi,_) = dest_state(state,i)
-          val n = length(Logic.strip_assums_hyp Bi) - 1
+fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
+      let val n = length(Logic.strip_assums_hyp Bi) - 1
           val (k,symopt) = eq_var bnd Bi
       in 
-         EVERY [REPEAT_DETERM_N k (etac rev_mp i),
-                etac revcut_rl i,
-                REPEAT_DETERM_N (n-k) (etac rev_mp i),
-                etac (symopt RS subst) i,
-                REPEAT_DETERM_N n (rtac imp_intr i)]
+         DETERM
+           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
+		   etac revcut_rl i,
+		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
+		   etac (symopt RS subst) i,
+		   REPEAT_DETERM_N n (rtac imp_intr i)])
       end
-      handle THM _ => no_tac | EQ_VAR => no_tac));
+      handle THM _ => no_tac | EQ_VAR => no_tac);
 
 (*Substitutes for Free or Bound variables*)
 val hyp_subst_tac = gen_hyp_subst_tac false;

--- a/src/FOLP/simp.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/FOLP/simp.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -202,15 +202,15 @@
     val hvars = foldr it_asms (asms,hvars)
     val hvs = map (#1 o dest_Var) hvars
     val refl1_tac = refl_tac 1
-    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
-              (STATE(fn thm =>
-                case head_of(rhs_of_eq 1 thm) of
-                  Var(ixn,_) => if ixn mem hvs then refl1_tac
-                                else resolve_tac normI_thms 1 ORELSE refl1_tac
-                | Const _ => resolve_tac normI_thms 1 ORELSE
-                             resolve_tac congs 1 ORELSE refl1_tac
-                | Free _ => resolve_tac congs 1 ORELSE refl1_tac
-                | _ => refl1_tac))
+    fun norm_step_tac st = st |>
+	 (case head_of(rhs_of_eq 1 st) of
+	    Var(ixn,_) => if ixn mem hvs then refl1_tac
+			  else resolve_tac normI_thms 1 ORELSE refl1_tac
+	  | Const _ => resolve_tac normI_thms 1 ORELSE
+		       resolve_tac congs 1 ORELSE refl1_tac
+	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
+	  | _ => refl1_tac)
+    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
     val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
 in thm'' end;
 

--- a/src/HOL/Hoare/Hoare.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -68,9 +68,10 @@
 (* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
    mit Namen von in nach um *)
 
-fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s
-                                                then Abs (nach,t,rename_abs (von,nach,trm))
-                                                else Abs (s,t,rename_abs (von,nach,trm))
+fun rename_abs (von,nach,Abs (s,t,trm)) =
+    if von=s
+	then Abs (nach,t,rename_abs (von,nach,trm))
+        else Abs (s,t,rename_abs (von,nach,trm))
   | rename_abs (von,nach,trm1 $ trm2)   =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
   | rename_abs (_,_,trm)                =trm;
 
@@ -85,41 +86,35 @@
 
 fun ren_abs_thm (von,nach,theorem)      =
         equal_elim
-                (
-                        reflexive (
-                                cterm_of
-                                        (#sign (rep_thm theorem))
-                                        (rename_abs (von,nach,#prop (rep_thm theorem)))
-                        )
-                )
+                (reflexive (cterm_of (#sign (rep_thm theorem))
+			    (rename_abs (von,nach,#prop (rep_thm theorem)))))
                 theorem;
 
 
-(**************************************************************************************************)
-(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch                         ***)
-(***  - Umbenennen von Lambda-Abstraktionen im Theorem                                          ***)
-(***  - Instanziieren von freien Variablen im Theorem                                           ***)
-(***  - Composing des Subgoals mit dem Theorem                                                  ***)
-(**************************************************************************************************)
+(****************************************************************************)
+(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch   ***)
+(***  - Umbenennen von Lambda-Abstraktionen im Theorem                    ***)
+(***  - Instanziieren von freien Variablen im Theorem                     ***)
+(***  - Composing des Subgoals mit dem Theorem                            ***)
+(****************************************************************************)
 
 (* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
    - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
 
 fun comp_inst_ren_tac rens insts theorem i      =
-        let
-                fun compose_inst_ren_tac [] insts theorem i                     =
-                        compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
-                  | compose_inst_ren_tac ((von,nach)::rl) insts theorem i       =
-                        compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
-        in
-                compose_inst_ren_tac rens insts theorem i
-        end;
+        let fun compose_inst_ren_tac [] insts theorem i                     =
+	      compose_tac (false,
+			   cterm_instantiate insts theorem,nprems_of theorem) i
+	      | compose_inst_ren_tac ((von,nach)::rl) insts theorem i       =
+                        compose_inst_ren_tac rl insts 
+			  (ren_abs_thm (von,nach,theorem)) i
+        in  compose_inst_ren_tac rens insts theorem i  end;
 
 
-(**************************************************************************************************)
+(***************************************************************    *********)
 (*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen                               ***)
 (***    Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1"               ***)
-(**************************************************************************************************)
+(****************************************************************************)
 
 (* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
    aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
@@ -127,97 +122,79 @@
               wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
 
 fun pvars_of_term (name,trm)    =
-        let
-                fun add_vars (name,Free (s,t) $ trm,vl) =if name=s
-                                                                then if trm mem vl
-                                                                        then vl
-                                                                        else trm::vl
-                                                                else add_vars (name,trm,vl)
-                  | add_vars (name,Abs (s,t,trm),vl)    =add_vars (name,trm,vl)
-                  | add_vars (name,trm1 $ trm2,vl)      =add_vars (name,trm2,add_vars (name,trm1,vl))
-                  | add_vars (_,_,vl)                   =vl
-        in
-                add_vars (name,trm,[])
-        end;
+  let fun add_vars (name,Free (s,t) $ trm,vl) =
+            if name=s then if trm mem vl then vl else trm::vl
+                      else add_vars (name,trm,vl)
+	| add_vars (name,Abs (s,t,trm),vl)    =add_vars (name,trm,vl)
+	| add_vars (name,trm1 $ trm2,vl)      =add_vars (name,trm2,add_vars (name,trm1,vl))
+	| add_vars (_,_,vl)                   =vl
+  in add_vars (name,trm,[]) end;
+
 
 (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
-   - v::vl:(term) list  Liste der zu eliminierenden Programmvariablen
-   - meta_spec:thm      Theorem, welches zur Entfernung der Variablen benutzt wird
-                        z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
-   - namexAll:string    Name von    ^                                  (hier "x")
-   - varx:term          Term zu                                      ^ (hier Var(("x",0),...))
-   - varP:term          Term zu                                  ^     (hier Var(("P",0),...))
-   - type_pvar:typ      Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
+ - v::vl:(term) list  Liste der zu eliminierenden Programmvariablen
+ - meta_spec:thm      Theorem, welches zur Entfernung der Variablen benutzt wird
+		      z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+ - namexAll:string    Name von    ^                                  (hier "x")
+ - varx:term          Term zu                                      ^ (hier Var(("x",0),...))
+ - varP:term          Term zu                                  ^     (hier Var(("P",0),...))
+ - type_pvar:typ      Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
 
-   Vorgehen:
-        - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
-        - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
-          z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
-                meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
-        - Instanziierungen in meta_spec:
-                varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
-                varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
-                 -      zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
-                        trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
-                 -      substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
-                        trm1 = "s(Suc(0)) = xs ==> xs = 1"
-                 -      abstrahiere ueber xs:
-                        trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
-                 -      abstrahiere ueber restliche Vorkommen von s:
-                        trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
-                 -      instanziiere varP mit trm3
+ Vorgehen:
+      - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
+      - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
+	z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
+	      meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
+      - Instanziierungen in meta_spec:
+	      varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
+	      varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
+	 - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
+		trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
+	 - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
+		trm1 = "s(Suc(0)) = xs ==> xs = 1"
+	 - abstrahiere ueber xs:
+		trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
+	 - abstrahiere ueber restliche Vorkommen von s:
+		trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
+	 - instanziiere varP mit trm3
 *)
 
-fun VarsElimTac ([],_,_,_,_,_) i                                        =all_tac
-  | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i        =
-        STATE (
-                fn state =>
-                comp_inst_ren_tac
-                        [(namexAll,pvar2pvarID v)]
-                        [(
-                                cterm_of (#sign (rep_thm state)) varx,
-                                cterm_of (#sign (rep_thm state)) (
-                                        Abs  ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
-                                )
-                        ),(
-                                cterm_of (#sign (rep_thm state)) varP,
-                                cterm_of (#sign (rep_thm state)) (
-                                        let
-                                                val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
-                                                val (sname,trm0) = variant_abs ("s",dummyT,trm);
-                                                val xsname = variant_name ("xs",trm0);
-                                                val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
-                                                val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
-                                        in
-                                                Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
-                                        end
-                                )
-                        )]
-                        meta_spec i
-        )
-        THEN
-        (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
-
-(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
-
-   zur Erinnerung:
-    -   das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
-        d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
-    -   meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+(* StateElimTac: tactic to eliminate all program variable from subgoal i
+    - applies to subgoals of the form "!!s:('a) state.P(s)",
+        i.e. the term  Const("all",_) $ Abs ("s",pvar --> 'a,_)
+    -   meta_spec has the form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
 *)
 
-fun StateElimTac i      =
-        STATE (
-                fn state =>
-                let
-                        val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
-                        val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
-                                (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
-                in
-                        VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
-                end
-        );
-
+val StateElimTac = SUBGOAL (fn (Bi,i) =>
+  let val Const _ $ Abs (_,Type ("fun",[_,type_pvar]),trm) = Bi
+      val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
+			    (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = 
+			    #prop (rep_thm meta_spec)
+      fun vtac v i st = st |>
+	  let val cterm = cterm_of (#sign (rep_thm st))
+	      val (_,_,_ $ Abs (_,_,trm),_) = dest_state (st,i);
+	      val (sname,trm0) = variant_abs ("s",dummyT,trm);
+	      val xsname = variant_name ("xs",trm0);
+	      val trm1 = subst_term (Free (sname,dummyT) $ v,
+				     Syntax.free xsname,trm0)
+	      val trm2 = Abs ("xs", type_pvar,
+			      abstract_over (Syntax.free xsname,trm1))
+	  in
+	      comp_inst_ren_tac
+		[(namexAll,pvar2pvarID v)]
+		[(cterm varx,
+		  cterm (Abs  ("s",Type ("nat",[]) --> type_pvar,
+			       Bound 0 $ v))),
+		 (cterm varP,
+		  cterm (Abs ("s", Type ("nat",[]) --> type_pvar,
+			      abstract_over (Free (sname,dummyT),trm2))))]
+		meta_spec i
+	  end
+      fun vars_tac [] i      = all_tac
+	| vars_tac (v::vl) i = vtac v i THEN vars_tac vl i
+  in
+      vars_tac (pvars_of_term (variant_abs ("s",dummyT,trm))) i
+  end);
 
 
 (*** tactics for verification condition generation ***)
@@ -228,25 +205,22 @@
    Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
 
 fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
-and HoareRuleTac i pre_cond =
-      STATE(fn state =>
-                ((WlpTac i) THEN (HoareRuleTac i pre_cond))
-                ORELSE
-                (FIRST[rtac SkipRule i,
-                       rtac AssignRule i,
-                       EVERY[rtac IfRule i,
-                             HoareRuleTac (i+2) false,
-                             HoareRuleTac (i+1) false],
-                       EVERY[rtac WhileRule i,
-                             Asm_full_simp_tac (i+2),
-                             HoareRuleTac (i+1) true]]
-                 THEN
-                 (if pre_cond then (Asm_full_simp_tac i) else (atac i))
-                )
-        );
+and HoareRuleTac i pre_cond st = st |>  
+	(*abstraction over st prevents looping*)
+    ( (WlpTac i THEN HoareRuleTac i pre_cond)
+      ORELSE
+      (FIRST[rtac SkipRule i,
+	     rtac AssignRule i,
+	     EVERY[rtac IfRule i,
+		   HoareRuleTac (i+2) false,
+		   HoareRuleTac (i+1) false],
+	     EVERY[rtac WhileRule i,
+		   Asm_full_simp_tac (i+2),
+		   HoareRuleTac (i+1) true]]
+       THEN
+       (if pre_cond then (Asm_full_simp_tac i) else (atac i))) );
 
-val HoareTac1 =
-  EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
+val hoare_tac = 
+  SELECT_GOAL
+    (EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]);
 
-val hoare_tac = SELECT_GOAL (HoareTac1);
-

--- a/src/HOL/ex/meson.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/HOL/ex/meson.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -245,8 +245,8 @@
   handle THM _ => (*disjunction?*)
     let val tac = 
         (METAHYPS (resop (cnf_nil seen)) 1) THEN
-        (STATE (fn st' => 
-                METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))
+        (fn st' => st' |>
+                METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
     in  Sequence.list_of_s (tac (th RS disj_forward)) @ ths  end
 and cnf_nil seen th = cnf_aux seen (th,[]);
 

--- a/src/Provers/classical.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/Provers/classical.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -595,7 +595,7 @@
   biresolve_from_nets_tac dup_netpair;
 
 (*Searching to depth m.*)
-fun depth_tac cs m i = STATE(fn state => 
+fun depth_tac cs m i state = 
   SELECT_GOAL 
    (getWrapper cs
     (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
@@ -605,7 +605,7 @@
       COND (K(m=0)) no_tac
         ((instp_step_tac cs i APPEND dup_step_tac cs i)
 	 THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1)
-  i);
+  i state;
 
 (*Search, with depth bound m.  
   This is the "entry point", which does safe inferences first.*)

--- a/src/Provers/hypsubst.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/Provers/hypsubst.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -116,12 +116,11 @@
   since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
   must NOT be deleted.  Tactic must rotate or delete m assumptions.
 *)
-fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
+fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
     let fun count []      = 0
 	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
 			      1 + count Bs)
                              handle Match => 0)
-	val (_,_,Bi,_) = dest_state(state,i)
         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
     in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
     end);
@@ -141,17 +140,16 @@
 
   (*Select a suitable equality assumption and substitute throughout the subgoal
     Replaces only Bound variables if bnd is true*)
-  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
-	let val (_,_,Bi,_) = dest_state(state,i)
-	    val n = length(Logic.strip_assums_hyp Bi) - 1
+  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
+	let val n = length(Logic.strip_assums_hyp Bi) - 1
 	    val (k,_) = eq_var bnd true Bi
 	in 
-	   EVERY [rotate_tac k i,
-		  asm_full_simp_tac hyp_subst_ss i,
-		  etac thin_rl i,
-		  thin_leading_eqs_tac bnd (n-k) i]
+	   DETERM (EVERY [rotate_tac k i,
+			  asm_full_simp_tac hyp_subst_ss i,
+			  etac thin_rl i,
+			  thin_leading_eqs_tac bnd (n-k) i])
 	end
-	handle THM _ => no_tac | EQ_VAR => no_tac));
+	handle THM _ => no_tac | EQ_VAR => no_tac);
 
 end;
 
@@ -159,18 +157,18 @@
 
 (*Old version of the tactic above -- slower but the only way
   to handle equalities containing Vars.*)
-fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
-      let val (_,_,Bi,_) = dest_state(state,i)
-	  val n = length(Logic.strip_assums_hyp Bi) - 1
+fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
+      let val n = length(Logic.strip_assums_hyp Bi) - 1
 	  val (k,symopt) = eq_var bnd false Bi
       in 
-	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
-		etac revcut_rl i,
-		REPEAT_DETERM_N (n-k) (etac rev_mp i),
-		etac (if symopt then ssubst else subst) i,
-		REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]
+	 DETERM
+           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
+		   etac revcut_rl i,
+		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
+		   etac (if symopt then ssubst else subst) i,
+		   REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)])
       end
-      handle THM _ => no_tac | EQ_VAR => no_tac));
+      handle THM _ => no_tac | EQ_VAR => no_tac);
 
 (*Substitutes for Free or Bound variables*)
 val hyp_subst_tac = 

--- a/src/Provers/simp.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/Provers/simp.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -196,15 +196,15 @@
     val hvars = foldr it_asms (asms,hvars)
     val hvs = map (#1 o dest_Var) hvars
     val refl1_tac = refl_tac 1
-    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
-	      (STATE(fn thm =>
-		case head_of(rhs_of_eq 1 thm) of
-		  Var(ixn,_) => if ixn mem hvs then refl1_tac
-				else resolve_tac normI_thms 1 ORELSE refl1_tac
-		| Const _ => resolve_tac normI_thms 1 ORELSE
-			     resolve_tac congs 1 ORELSE refl1_tac
-		| Free _ => resolve_tac congs 1 ORELSE refl1_tac
-		| _ => refl1_tac))
+    fun norm_step_tac st = st |>
+	 (case head_of(rhs_of_eq 1 st) of
+	    Var(ixn,_) => if ixn mem hvs then refl1_tac
+			  else resolve_tac normI_thms 1 ORELSE refl1_tac
+	  | Const _ => resolve_tac normI_thms 1 ORELSE
+		       resolve_tac congs 1 ORELSE refl1_tac
+	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
+	  | _ => refl1_tac))
+    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
     val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
 in thm'' end;
 

--- a/src/Provers/simplifier.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/Provers/simplifier.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -272,9 +272,8 @@
 
 (** simplification tactics **)
 
-fun NEWSUBGOALS tac tacf =
-  STATE (fn state0 =>
-    tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0)));
+fun NEWSUBGOALS tac tacf st0 = st0 |>
+    (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
 
 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
 fun basic_gen_simp_tac mode =

--- a/src/Provers/splitter.ML	Fri Jul 18 14:06:54 1997 +0200
+++ b/src/Provers/splitter.ML	Tue Jul 22 11:12:55 1997 +0200
@@ -261,21 +261,21 @@
                            val (Const(a,_),args) = strip_comb lhs
                        in (a,(thm,fastype_of t,length args)) end
       val cmap = map const splits;
-      fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
-      fun lift_split state =
-            let val (Ts,t,splits) = select cmap state i
+      fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
+      fun lift_split_tac st = st |>
+            let val (Ts,t,splits) = select cmap st i
             in case splits of
                  [] => no_tac
                | (thm,apsns,pos,TB,tt)::_ =>
                    (case apsns of
-                      [] => STATE(fn state => rtac (inst_split Ts t tt thm TB state) i)
-                    | p::_ => EVERY[STATE(lift Ts t p),
+                      [] => (fn state => state |>
+			           rtac (inst_split Ts t tt thm TB state) i)
+                    | p::_ => EVERY[lift_tac Ts t p,
                                     rtac reflexive_thm (i+1),
-                                    STATE lift_split])
+                                    lift_split_tac])
             end
-  in STATE(fn thm =>
-       if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
-       else no_tac)
+  in COND (has_fewer_prems i) no_tac 
+          (rtac iffD i THEN lift_split_tac)
   end;
 
 in split_tac end;