Now uses rotate_tac and eta_contract_atom for greater speed
authorpaulson
Wed Mar 05 10:01:57 1997 +0100 (1997-03-05 ago)
changeset 27223e07c20b967c
parent 2721 f08042e18c7d
child 2723 f09ecc2cd3f1
Now uses rotate_tac and eta_contract_atom for greater speed
src/Provers/hypsubst.ML
     1.1 --- a/src/Provers/hypsubst.ML	Wed Mar 05 09:59:55 1997 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Wed Mar 05 10:01:57 1997 +0100
     1.3 @@ -47,6 +47,8 @@
     1.4    val thin_leading_eqs_tac   : bool -> int -> int -> tactic
     1.5    end;
     1.6  
     1.7 +
     1.8 +
     1.9  functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
    1.10  struct
    1.11  
    1.12 @@ -62,7 +64,7 @@
    1.13    change it back (any Bound variable will do)
    1.14  *)
    1.15  fun contract t =
    1.16 -    case Pattern.eta_contract t of
    1.17 +    case Pattern.eta_contract_atom t of
    1.18  	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
    1.19        | t'        => t'
    1.20  end;
    1.21 @@ -121,8 +123,7 @@
    1.22                               handle Match => 0)
    1.23  	val (_,_,Bi,_) = dest_state(state,i)
    1.24          val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
    1.25 -    in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
    1.26 -        REPEAT_DETERM_N (m-j) (etac revcut_rl i)
    1.27 +    in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
    1.28      end);
    1.29  
    1.30  (*For the simpset.  Adds ALL suitable equalities, even if not first!
    1.31 @@ -145,7 +146,7 @@
    1.32  	    val n = length(Logic.strip_assums_hyp Bi) - 1
    1.33  	    val (k,_) = eq_var bnd true Bi
    1.34  	in 
    1.35 -	   EVERY [REPEAT_DETERM_N k (etac revcut_rl i),
    1.36 +	   EVERY [rotate_tac k i,
    1.37  		  asm_full_simp_tac hyp_subst_ss i,
    1.38  		  etac thin_rl i,
    1.39  		  thin_leading_eqs_tac bnd (n-k) i]