607 

   607 

   608   the name of the constant @{text "Nil"} depends on the theory in which the

   608   the name of the constant @{text "Nil"} depends on the theory in which the

   609   term constructor is defined (@{text "List"}) and also in which datatype

   609   term constructor is defined (@{text "List"}) and also in which datatype

   610   (@{text "list"}). Even worse, some constants have a name involving

   610   (@{text "list"}). Even worse, some constants have a name involving

   611   type-classes. Consider for example the constants for @{term "zero"} and

   611   type-classes. Consider for example the constants for @{term "zero"} and

   615  "(Const (\"Groups.zero_class.zero\", \<dots>), 

   615  "(Const (\"Groups.zero_class.zero\", \<dots>), 

   616  Const (\"Groups.times_class.times\", \<dots>))"}

   616  Const (\"Groups.times_class.times\", \<dots>))"}

   617 

   617 

   618   While you could use the complete name, for example 

   618   While you could use the complete name, for example 

   619   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or

   619   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or

  2131   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 

  2131   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 

  2132   install this function as the theorem style named @{text "my_strip_allq"}. 

  2132   install this function as the theorem style named @{text "my_strip_allq"}. 

  2133 *}

  2133 *}

  2134 

  2134 

  2135 setup %gray{* 

  2135 setup %gray{* 

  2137 *}

  2137 *}

  2138 

  2138 

  2139 text {*

  2139 text {*

  2140   We can test this theorem style with the following theorem

  2140   We can test this theorem style with the following theorem

  2141 *}

  2141 *}

  2183 

  2183 

  2184 setup %gray {* let

  2184 setup %gray {* let

  2185   val parser = Scan.repeat Args.name

  2185   val parser = Scan.repeat Args.name

  2186   fun action xs = K (rename_allq xs #> strip_allq)

  2186   fun action xs = K (rename_allq xs #> strip_allq)

  2187 in

  2187 in

  2189 end *}

  2189 end *}

  2190 

  2190 

  2191 text {*

  2191 text {*

  2192   The parser reads a list of names. In the function @{text action} we first

  2192   The parser reads a list of names. In the function @{text action} we first

  2193   call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}

  2193   call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}