# HG changeset patch
# User wenzelm
# Date 1364660841 -3600
# Node ID e4aeb102ad70d39237ab31a33780ae43796aec27
# Parent  c52891242de2196b33c615bfce3f4d7722115b5a
amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;

diff -r c52891242de2 -r e4aeb102ad70 src/Pure/raw_simplifier.ML
--- 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.