Optimized unfold_attr.
authorberghofe
Tue Sep 27 12:13:17 2005 +0200 (2005-09-27)
changeset 176664708ab4626a5
parent 17665 64e5aecbf7fd
child 17667 2beb71c0f92e
Optimized unfold_attr.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Tue Sep 27 11:39:27 2005 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Sep 27 12:13:17 2005 +0200
     1.3 @@ -346,12 +346,15 @@
     1.4      
     1.5  fun unfold_attr (thy, eqn) =
     1.6    let
     1.7 -    val (name, _) = dest_Const (head_of
     1.8 -      (fst (Logic.dest_equals (prop_of eqn))));
     1.9 +    val names = term_consts
    1.10 +      (fst (Logic.dest_equals (prop_of eqn)));
    1.11      fun prep thy = map (fn th =>
    1.12 -      if name mem term_consts (prop_of th) then
    1.13 -        rewrite_rule [eqn] (Thm.transfer thy th)
    1.14 -      else th)
    1.15 +      let val prop = prop_of th
    1.16 +      in
    1.17 +        if forall (fn name => exists_Const (equal name o fst) prop) names
    1.18 +        then rewrite_rule [eqn] (Thm.transfer thy th)
    1.19 +        else th
    1.20 +      end)
    1.21    in (add_preprocessor prep thy, eqn) end;
    1.22  
    1.23  val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];