# HG changeset patch
# User krauss
# Date 1149587890 -7200
# Node ID fa5080577da95182671e36f02227668f5cf9a6c7
# Parent  82f365a14960ac3d49d29781de681ae4b407d0ff
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.

diff -r 82f365a14960 -r fa5080577da9 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 10:05:57 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 11:58:10 2006 +0200
@@ -116,7 +116,10 @@
 	val tsimps = map (map remove_domain_condition) psimps
 	val tinduct = map remove_domain_condition simple_pinducts
 
-        val thy = fold2 (add_simps "simps" [(*RecfunCodegen.add NONE*)]) (parts ~~ tsimps) (names ~~ atts) thy
+        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
+        val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
+
+        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) (names ~~ atts) thy
 
 	val thy = Theory.add_path name thy