equal
deleted
inserted
replaced
1007 "@{type_name \"list\"}" "\"List.list\""} |
1007 "@{type_name \"list\"}" "\"List.list\""} |
1008 |
1008 |
1009 (FIXME: Explain the following better.) |
1009 (FIXME: Explain the following better.) |
1010 |
1010 |
1011 Occasionally you have to calculate what the ``base'' name of a given |
1011 Occasionally you have to calculate what the ``base'' name of a given |
1012 constant is. For this you can use the function @{ML [index] extern_const in Sign} or |
1012 constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or |
1013 @{ML base_name in Long_Name}. For example: |
1013 @{ML [index] Long_Name.base_name}. For example: |
1014 |
1014 |
1015 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
1015 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
1016 |
1016 |
1017 The difference between both functions is that @{ML extern_const in Sign} returns |
1017 The difference between both functions is that @{ML extern_const in Sign} returns |
1018 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |
1018 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |