src/Provers/hypsubst.ML
changeset 3537 79ac9b475621
parent 2750 fe3799355b5e
child 4179 cc4b6791d5dc
     1.1 --- a/src/Provers/hypsubst.ML	Fri Jul 18 14:06:54 1997 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Tue Jul 22 11:12:55 1997 +0200
     1.3 @@ -116,12 +116,11 @@
     1.4    since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
     1.5    must NOT be deleted.  Tactic must rotate or delete m assumptions.
     1.6  *)
     1.7 -fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
     1.8 +fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
     1.9      let fun count []      = 0
    1.10  	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
    1.11  			      1 + count Bs)
    1.12                               handle Match => 0)
    1.13 -	val (_,_,Bi,_) = dest_state(state,i)
    1.14          val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
    1.15      in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
    1.16      end);
    1.17 @@ -141,17 +140,16 @@
    1.18  
    1.19    (*Select a suitable equality assumption and substitute throughout the subgoal
    1.20      Replaces only Bound variables if bnd is true*)
    1.21 -  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    1.22 -	let val (_,_,Bi,_) = dest_state(state,i)
    1.23 -	    val n = length(Logic.strip_assums_hyp Bi) - 1
    1.24 +  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    1.25 +	let val n = length(Logic.strip_assums_hyp Bi) - 1
    1.26  	    val (k,_) = eq_var bnd true Bi
    1.27  	in 
    1.28 -	   EVERY [rotate_tac k i,
    1.29 -		  asm_full_simp_tac hyp_subst_ss i,
    1.30 -		  etac thin_rl i,
    1.31 -		  thin_leading_eqs_tac bnd (n-k) i]
    1.32 +	   DETERM (EVERY [rotate_tac k i,
    1.33 +			  asm_full_simp_tac hyp_subst_ss i,
    1.34 +			  etac thin_rl i,
    1.35 +			  thin_leading_eqs_tac bnd (n-k) i])
    1.36  	end
    1.37 -	handle THM _ => no_tac | EQ_VAR => no_tac));
    1.38 +	handle THM _ => no_tac | EQ_VAR => no_tac);
    1.39  
    1.40  end;
    1.41  
    1.42 @@ -159,18 +157,18 @@
    1.43  
    1.44  (*Old version of the tactic above -- slower but the only way
    1.45    to handle equalities containing Vars.*)
    1.46 -fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    1.47 -      let val (_,_,Bi,_) = dest_state(state,i)
    1.48 -	  val n = length(Logic.strip_assums_hyp Bi) - 1
    1.49 +fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    1.50 +      let val n = length(Logic.strip_assums_hyp Bi) - 1
    1.51  	  val (k,symopt) = eq_var bnd false Bi
    1.52        in 
    1.53 -	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    1.54 -		etac revcut_rl i,
    1.55 -		REPEAT_DETERM_N (n-k) (etac rev_mp i),
    1.56 -		etac (if symopt then ssubst else subst) i,
    1.57 -		REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]
    1.58 +	 DETERM
    1.59 +           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    1.60 +		   etac revcut_rl i,
    1.61 +		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    1.62 +		   etac (if symopt then ssubst else subst) i,
    1.63 +		   REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)])
    1.64        end
    1.65 -      handle THM _ => no_tac | EQ_VAR => no_tac));
    1.66 +      handle THM _ => no_tac | EQ_VAR => no_tac);
    1.67  
    1.68  (*Substitutes for Free or Bound variables*)
    1.69  val hyp_subst_tac =