| changeset 47815 | 43f677b3ae91 |
| parent 46961 | 5c6955f487e5 |
| child 51930 | 52fd62618631 |
--- a/src/ZF/Tools/primrec_package.ML Fri Apr 27 21:47:47 2012 +0200 +++ b/src/ZF/Tools/primrec_package.ML Fri Apr 27 22:47:30 2012 +0200 @@ -189,7 +189,7 @@ fun add_primrec args thy = add_primrec_i (map (fn ((name, s), srcs) => - ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs)) + ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs)) args) thy;