HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
authorkrauss
Tue Jun 06 11:58:10 2006 +0200 (2006-06-06)
changeset 19784fa5080577da9
parent 19783 82f365a14960
child 19785 52d71ee5c8a8
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 10:05:57 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 11:58:10 2006 +0200
     1.3 @@ -116,7 +116,10 @@
     1.4  	val tsimps = map (map remove_domain_condition) psimps
     1.5  	val tinduct = map remove_domain_condition simple_pinducts
     1.6  
     1.7 -        val thy = fold2 (add_simps "simps" [(*RecfunCodegen.add NONE*)]) (parts ~~ tsimps) (names ~~ atts) thy
     1.8 +        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
     1.9 +        val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
    1.10 +
    1.11 +        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) (names ~~ atts) thy
    1.12  
    1.13  	val thy = Theory.add_path name thy
    1.14