src/Provers/hypsubst.ML

   val inspect_pair           : bool -> bool -> term * term -> bool
   val mk_eqs                 : thm -> thm list
   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
   end;
 
+
+
 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
 struct
 
 local open Data in
 

 in
 (*Simplifier turns Bound variables to dotted Free variables: 
   change it back (any Bound variable will do)
 *)
 fun contract t =
-    case Pattern.eta_contract t of
+    case Pattern.eta_contract_atom t of
 	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
       | t'        => t'
 end;
 
 fun has_vars t = maxidx_of_term t <> ~1;

 	  | 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
-        REPEAT_DETERM_N (m-j) (etac revcut_rl i)
+    in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
     end);
 
 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   No vars are allowed here, as simpsets are built from meta-assumptions*)
 fun mk_eqs th = 

   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
 	    val (k,_) = eq_var bnd true Bi
 	in 
-	   EVERY [REPEAT_DETERM_N k (etac revcut_rl i),
+	   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));