src/Provers/hypsubst.ML
changeset 2143 093bbe6d333b
parent 1011 5c9654e2e3de
child 2174 0829b7b632c5
equal deleted inserted replaced
2142:20f208ff085d 2143:093bbe6d333b
   118     let fun count []      = 0
   118     let fun count []      = 0
   119 	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
   119 	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
   120 			      1 + count Bs)
   120 			      1 + count Bs)
   121                              handle Match => 0)
   121                              handle Match => 0)
   122 	val (_,_,Bi,_) = dest_state(state,i)
   122 	val (_,_,Bi,_) = dest_state(state,i)
   123         val j = min [m, count (Logic.strip_assums_hyp Bi)]
   123         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
   124     in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
   124     in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
   125         REPEAT_DETERM_N (m-j) (etac revcut_rl i)
   125         REPEAT_DETERM_N (m-j) (etac revcut_rl i)
   126     end);
   126     end);
   127 
   127 
   128 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   128 (*For the simpset.  Adds ALL suitable equalities, even if not first!