src/HOL/Tools/function_package/fundef_package.ML
changeset 19782 48c4632e2c28
parent 19770 be5c23ebe1eb
child 19784 fa5080577da9
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 08:21:14 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 06 09:28:24 2006 +0200
     1.3 @@ -116,7 +116,7 @@
     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 thy = fold2 (add_simps "simps" [(*RecfunCodegen.add NONE*)]) (parts ~~ tsimps) (names ~~ atts) thy
     1.9  
    1.10  	val thy = Theory.add_path name thy
    1.11