src/HOL/Library/LaTeXsugar.thy
changeset 69593 3dda49e08b9d
parent 69592 a80d8ec6c998
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -112,13 +112,13 @@
     1.4      let
     1.5        val rhs_vars = Term.add_vars rhs [];
     1.6        fun dummy (v as Var (ixn as (_, T))) =
     1.7 -            if member ((=) ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T)
     1.8 +            if member ((=) ) rhs_vars ixn then v else Const (\<^const_name>\<open>DUMMY\<close>, T)
     1.9          | dummy (t $ u) = dummy t $ dummy u
    1.10          | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
    1.11          | dummy t = t;
    1.12      in wrap $ (eq $ dummy lhs $ rhs) end
    1.13  in
    1.14 -  Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats))
    1.15 +  Term_Style.setup \<^binding>\<open>dummy_pats\<close> (Scan.succeed (K dummy_pats))
    1.16  end
    1.17  \<close>
    1.18  
    1.19 @@ -145,7 +145,7 @@
    1.20  val style_eta_expand =
    1.21    (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))
    1.22  
    1.23 -in Term_Style.setup @{binding eta_expand} style_eta_expand end
    1.24 +in Term_Style.setup \<^binding>\<open>eta_expand\<close> style_eta_expand end
    1.25  \<close>
    1.26  
    1.27  end