Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
authorkrauss
Tue, 06 Jun 2006 11:58:10 +0200
changeset 19784 fa5080577da9
parent 19783 82f365a14960
child 19785 52d71ee5c8a8
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
src/HOL/Tools/function_package/fundef_package.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle