37 using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example |
37 using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example |
38 |
38 |
39 @{ML_response [display,gray] |
39 @{ML_response [display,gray] |
40 "@{term \"(a::nat) + b = c\"}" |
40 "@{term \"(a::nat) + b = c\"}" |
41 "Const (\"op =\", \<dots>) $ |
41 "Const (\"op =\", \<dots>) $ |
42 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
42 (Const (\"Algebras.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
43 |
43 |
44 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using |
44 constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using |
45 the internal representation corresponding to the datatype @{ML_type_ind "term"}, |
45 the internal representation corresponding to the datatype @{ML_type_ind "term"}, |
46 which is defined as follows: |
46 which is defined as follows: |
47 *} |
47 *} |
531 (@{text "list"}). Even worse, some constants have a name involving |
531 (@{text "list"}). Even worse, some constants have a name involving |
532 type-classes. Consider for example the constants for @{term "zero"} and |
532 type-classes. Consider for example the constants for @{term "zero"} and |
533 \mbox{@{text "(op *)"}}: |
533 \mbox{@{text "(op *)"}}: |
534 |
534 |
535 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" |
535 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" |
536 "(Const (\"HOL.zero_class.zero\", \<dots>), |
536 "(Const (\"Algebras.zero_class.zero\", \<dots>), |
537 Const (\"HOL.times_class.times\", \<dots>))"} |
537 Const (\"Algebras.times_class.times\", \<dots>))"} |
538 |
538 |
539 While you could use the complete name, for example |
539 While you could use the complete name, for example |
540 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
540 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
541 matching against @{text "Nil"}, this would make the code rather brittle. |
541 matching against @{text "Nil"}, this would make the code rather brittle. |
542 The reason is that the theory and the name of the datatype can easily change. |
542 The reason is that the theory and the name of the datatype can easily change. |