src/HOL/Types_To_Sets/unoverload_type.ML
changeset 68434 c6a38342376e
parent 68433 f396f5490a8c
child 68435 2a2ef4552aaf
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:11:35 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:22:58 2018 +0200
     1.3 @@ -6,8 +6,8 @@
     1.4  
     1.5  signature UNOVERLOAD_TYPE =
     1.6  sig
     1.7 -  val unoverload_type: Context.generic -> indexname -> thm -> thm
     1.8 -  val unoverload_type_attr: indexname -> attribute
     1.9 +  val unoverload_type: Context.generic -> indexname list -> thm -> thm
    1.10 +  val unoverload_type_attr: indexname list -> attribute
    1.11  end;
    1.12  
    1.13  structure Unoverload_Type : UNOVERLOAD_TYPE =
    1.14 @@ -39,7 +39,7 @@
    1.15      (tvar, thm')
    1.16    end
    1.17  
    1.18 -fun unoverload_type context x thm =
    1.19 +fun unoverload_single_type context x thm =
    1.20    let
    1.21      val tvars = Term.add_tvars (Thm.prop_of thm) []
    1.22      val thy = Context.theory_of context
    1.23 @@ -56,9 +56,11 @@
    1.24      end
    1.25    end
    1.26  
    1.27 -fun unoverload_type_attr x = Thm.rule_attribute [] (fn context => unoverload_type context x)
    1.28 +fun unoverload_type context xs = fold (unoverload_single_type context) xs
    1.29 +
    1.30 +fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
    1.31  
    1.32  val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
    1.33 -  (Scan.lift Args.var >> unoverload_type_attr) "internalize a sort"))
    1.34 +  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) "internalize a sort"))
    1.35  
    1.36  end
    1.37 \ No newline at end of file