src/HOL/HOLCF/Fixrec.thy
changeset 69597 ff784d5a5bfb
parent 65380 ae93953746fc
child 69605 a96320074298
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -233,15 +233,15 @@
     1.4  
     1.5  setup \<open>
     1.6    Fixrec.add_matchers
     1.7 -    [ (@{const_name up}, @{const_name match_up}),
     1.8 -      (@{const_name sinl}, @{const_name match_sinl}),
     1.9 -      (@{const_name sinr}, @{const_name match_sinr}),
    1.10 -      (@{const_name spair}, @{const_name match_spair}),
    1.11 -      (@{const_name Pair}, @{const_name match_Pair}),
    1.12 -      (@{const_name ONE}, @{const_name match_ONE}),
    1.13 -      (@{const_name TT}, @{const_name match_TT}),
    1.14 -      (@{const_name FF}, @{const_name match_FF}),
    1.15 -      (@{const_name bottom}, @{const_name match_bottom}) ]
    1.16 +    [ (\<^const_name>\<open>up\<close>, \<^const_name>\<open>match_up\<close>),
    1.17 +      (\<^const_name>\<open>sinl\<close>, \<^const_name>\<open>match_sinl\<close>),
    1.18 +      (\<^const_name>\<open>sinr\<close>, \<^const_name>\<open>match_sinr\<close>),
    1.19 +      (\<^const_name>\<open>spair\<close>, \<^const_name>\<open>match_spair\<close>),
    1.20 +      (\<^const_name>\<open>Pair\<close>, \<^const_name>\<open>match_Pair\<close>),
    1.21 +      (\<^const_name>\<open>ONE\<close>, \<^const_name>\<open>match_ONE\<close>),
    1.22 +      (\<^const_name>\<open>TT\<close>, \<^const_name>\<open>match_TT\<close>),
    1.23 +      (\<^const_name>\<open>FF\<close>, \<^const_name>\<open>match_FF\<close>),
    1.24 +      (\<^const_name>\<open>bottom\<close>, \<^const_name>\<open>match_bottom\<close>) ]
    1.25  \<close>
    1.26  
    1.27  hide_const (open) succeed fail run