amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
1.1 --- a/src/Pure/raw_simplifier.ML Sat Mar 30 17:13:21 2013 +0100
1.2 +++ b/src/Pure/raw_simplifier.ML Sat Mar 30 17:27:21 2013 +0100
1.3 @@ -883,7 +883,10 @@
1.4
1.5 fun uncond_skel ((_, weak), (lhs, rhs)) =
1.6 if null weak then rhs (*optimization*)
1.7 - else if exists_Const (fn (c, _) => member (op =) weak (true, c)) lhs then skel0
1.8 + else if exists_subterm
1.9 + (fn Const (a, _) => member (op =) weak (true, a)
1.10 + | Free (a, _) => member (op =) weak (false, a)
1.11 + | _ => false) lhs then skel0
1.12 else rhs;
1.13
1.14 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.