| changeset 24707 | dfeb98f84e93 |
| parent 22101 | 6d13239d5f52 |
| child 24712 | 64ed05609568 |
--- a/src/ZF/Tools/primrec_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/ZF/Tools/primrec_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -197,7 +197,7 @@ fun add_primrec args thy = add_primrec_i (map (fn ((name, s), srcs) => - ((name, Sign.read_prop thy s), map (Attrib.attribute thy) srcs)) + ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs)) args) thy;