allow for a list of vars

--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:11:35 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:22:58 2018 +0200
@@ -6,8 +6,8 @@
 
 signature UNOVERLOAD_TYPE =
 sig
-  val unoverload_type: Context.generic -> indexname -> thm -> thm
-  val unoverload_type_attr: indexname -> attribute
+  val unoverload_type: Context.generic -> indexname list -> thm -> thm
+  val unoverload_type_attr: indexname list -> attribute
 end;
 
 structure Unoverload_Type : UNOVERLOAD_TYPE =
@@ -39,7 +39,7 @@
     (tvar, thm')
   end
 
-fun unoverload_type context x thm =
+fun unoverload_single_type context x thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
     val thy = Context.theory_of context
@@ -56,9 +56,11 @@
     end
   end
 
-fun unoverload_type_attr x = Thm.rule_attribute [] (fn context => unoverload_type context x)
+fun unoverload_type context xs = fold (unoverload_single_type context) xs
+
+fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
 
 val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
-  (Scan.lift Args.var >> unoverload_type_attr) "internalize a sort"))
+  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) "internalize a sort"))
 
 end
\ No newline at end of file