# HG changeset patch
# User immler
# Date 1528873895 -7200
# Node ID f396f5490a8c58d9d2e846f1ca5500e8cdee4233
# Parent  6f3bd27ba389e28809e68ed988e0ac93a3c26a6b
parse var

diff -r 6f3bd27ba389 -r f396f5490a8c src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:37:47 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:11:35 2018 +0200
@@ -6,8 +6,8 @@
 
 signature UNOVERLOAD_TYPE =
 sig
-  val unoverload_type: Context.generic -> string -> thm -> thm
-  val unoverload_type_attr: string -> attribute
+  val unoverload_type: Context.generic -> indexname -> thm -> thm
+  val unoverload_type_attr: indexname -> attribute
 end;
 
 structure Unoverload_Type : UNOVERLOAD_TYPE =
@@ -39,13 +39,13 @@
     (tvar, thm')
   end
 
-fun unoverload_type context s thm =
+fun unoverload_type context x thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
     val thy = Context.theory_of context
   in
-  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
-    raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
+  case find_first (fn (y, _) => x = y) tvars of NONE =>
+    raise THM ("unoverload_type: type variable ("^(@{make_string} x)^") not in theorem", 0, [thm])
   | SOME (x as (_, sort)) =>
     let
       val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
@@ -56,13 +56,9 @@
     end
   end
 
-val tyN = (Args.context -- Args.typ) >>
-  (fn (_, TFree (n, _)) => n
-  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
-
-fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
+fun unoverload_type_attr x = Thm.rule_attribute [] (fn context => unoverload_type context x)
 
 val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
-  (tyN >> unoverload_type_attr) "internalize a sort"))
+  (Scan.lift Args.var >> unoverload_type_attr) "internalize a sort"))
 
 end
\ No newline at end of file