991 term constructor is defined (@{text "List"}) and also in which datatype |
991 term constructor is defined (@{text "List"}) and also in which datatype |
992 (@{text "list"}). Even worse, some constants have a name involving |
992 (@{text "list"}). Even worse, some constants have a name involving |
993 type-classes. Consider for example the constants for @{term "zero"} and |
993 type-classes. Consider for example the constants for @{term "zero"} and |
994 \mbox{@{text "(op *)"}}: |
994 \mbox{@{text "(op *)"}}: |
995 |
995 |
996 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" |
996 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" |
997 "(Const (\"HOL.zero_class.zero\", \<dots>), |
997 "(Const (\"HOL.zero_class.zero\", \<dots>), |
998 Const (\"HOL.times_class.times\", \<dots>))"} |
998 Const (\"HOL.times_class.times\", \<dots>))"} |
999 |
999 |
1000 While you could use the complete name, for example |
1000 While you could use the complete name, for example |
1001 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
1001 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |