| changeset 30223 | 24d975352879 |
| parent 30173 | eabece26b89b |
| child 30242 | aea5d7fa7ef5 |
--- a/src/Pure/Isar/isar_cmd.ML Tue Mar 03 18:31:59 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 03 18:32:01 2009 +0100 @@ -161,7 +161,7 @@ (* axioms *) fun add_axms f args thy = - f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy; + f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy; val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);