equal
deleted
inserted
replaced
274 text {* |
274 text {* |
275 \footnote{\bf FIXME: Explain the following better; maybe put in a separate |
275 \footnote{\bf FIXME: Explain the following better; maybe put in a separate |
276 section and link with the comment in the antiquotation section.} |
276 section and link with the comment in the antiquotation section.} |
277 |
277 |
278 Occasionally you have to calculate what the ``base'' name of a given |
278 Occasionally you have to calculate what the ``base'' name of a given |
279 constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or |
279 constant is. For this you can use the function @{ML_ind "ProofContext.extern_const"} or |
280 @{ML_ind Long_Name.base_name}. For example: |
280 @{ML_ind Long_Name.base_name}. For example: |
281 |
281 |
282 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
282 @{ML_response [display,gray] "ProofContext.extern_const @{context} \"List.list.Nil\"" "\"Nil\""} |
283 |
283 |
284 The difference between both functions is that @{ML extern_const in Sign} returns |
284 The difference between both functions is that @{ML extern_const in ProofContext} returns |
285 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |
285 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |
286 strips off all qualifiers. |
286 strips off all qualifiers. |
287 |
287 |
288 \begin{readmore} |
288 \begin{readmore} |
289 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
289 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |