# HG changeset patch
# User berghofe
# Date 1127815997 -7200
# Node ID 4708ab4626a53c171bc29b18f86d531106df9367
# Parent  64e5aecbf7fdaef6dd174d11b5b403b7e5afd6d9
Optimized unfold_attr.

diff -r 64e5aecbf7fd -r 4708ab4626a5 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Sep 27 11:39:27 2005 +0200
+++ b/src/Pure/codegen.ML	Tue Sep 27 12:13:17 2005 +0200
@@ -346,12 +346,15 @@
     
 fun unfold_attr (thy, eqn) =
   let
-    val (name, _) = dest_Const (head_of
-      (fst (Logic.dest_equals (prop_of eqn))));
+    val names = term_consts
+      (fst (Logic.dest_equals (prop_of eqn)));
     fun prep thy = map (fn th =>
-      if name mem term_consts (prop_of th) then
-        rewrite_rule [eqn] (Thm.transfer thy th)
-      else th)
+      let val prop = prop_of th
+      in
+        if forall (fn name => exists_Const (equal name o fst) prop) names
+        then rewrite_rule [eqn] (Thm.transfer thy th)
+        else th
+      end)
   in (add_preprocessor prep thy, eqn) end;
 
 val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];