src/Provers/hypsubst.ML
 changeset 3537 79ac9b475621 parent 2750 fe3799355b5e child 4179 cc4b6791d5dc
```--- 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,
+	   DETERM (EVERY [rotate_tac k i,
+			  asm_full_simp_tac hyp_subst_ss i,
+			  etac thin_rl 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);