src/HOL/Types_To_Sets/unoverload_type.ML
changeset 69597 ff784d5a5bfb
parent 68438 f04d0e75e439
child 69688 33843320448f
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
     1.6  
     1.7 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
     1.8 +val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload_type\<close>
     1.9    (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
    1.10      "internalize and unoverload type class parameters"))
    1.11