amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;

--- a/src/Pure/raw_simplifier.ML	Sat Mar 30 17:13:21 2013 +0100
+++ b/src/Pure/raw_simplifier.ML	Sat Mar 30 17:27:21 2013 +0100
@@ -883,7 +883,10 @@
 
 fun uncond_skel ((_, weak), (lhs, rhs)) =
   if null weak then rhs  (*optimization*)
-  else if exists_Const (fn (c, _) => member (op =) weak (true, c)) lhs then skel0
+  else if exists_subterm
+    (fn Const (a, _) => member (op =) weak (true, a)
+      | Free (a, _) => member (op =) weak (false, a)
+      | _ => false) lhs then skel0
   else rhs;
 
 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.