tuned
authorimmler
Wed Jun 13 09:26:04 2018 +0200 (13 months ago)
changeset 684352a2ef4552aaf
parent 68434 c6a38342376e
child 68436 1b3edf5da4e4
tuned
src/HOL/Types_To_Sets/unoverload_type.ML
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:22:58 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:26:04 2018 +0200
     1.3 @@ -61,6 +61,7 @@
     1.4  fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
     1.5  
     1.6  val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
     1.7 -  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) "internalize a sort"))
     1.8 +  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
     1.9 +    "internalize and unoverload type class parameters"))
    1.10  
    1.11  end
    1.12 \ No newline at end of file