# 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)];