# HG changeset patch # User wenzelm # Date 1158858308 -7200 # Node ID 2aa8269a868ec436d519edefa69b4a082d671a97 # Parent 115262dd18e288284a0e1c52312f257235cf152a member (op =); Drule.dest_equals_rhs; diff -r 115262dd18e2 -r 2aa8269a868e src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu Sep 21 19:05:01 2006 +0200 +++ b/src/Pure/meta_simplifier.ML Thu Sep 21 19:05:08 2006 +0200 @@ -550,7 +550,7 @@ let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in is_Var x andalso forall is_Bound xs andalso null (findrep xs) andalso xs = ys andalso - (x, y) mem varpairs andalso + member (op =) varpairs (x, y) andalso is_full_cong_prems prems (remove (op =) (x, y) varpairs) end | _ => false); @@ -779,7 +779,7 @@ val dest_eq = Drule.dest_equals o Thm.cprop_of; val lhs_of = #1 o dest_eq; -val rhs_of = #2 o dest_eq; +val rhs_of = Drule.dest_equals_rhs o Thm.cprop_of; fun check_conv msg ss thm thm' = let @@ -821,7 +821,7 @@ fun uncond_skel ((_, weak), (lhs, rhs)) = if null weak then rhs (*optimization*) - else if exists_Const (fn (c, _) => c mem weak) lhs then skel0 + else if exists_Const (member (op =) weak o #1) lhs then skel0 else rhs; (*Behaves like unconditional rule if rhs does not contain vars not in the lhs. @@ -1124,7 +1124,8 @@ in mut_impc prems concl rrss asms (prem' :: prems') (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true) (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies - (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1 + (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) + ss (length prems') ~1 end (*legacy code - only for backwards compatibility*)