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