parse var
authorimmler
Wed Jun 13 09:11:35 2018 +0200 (11 months ago)
changeset 68433f396f5490a8c
parent 68432 6f3bd27ba389
child 68434 c6a38342376e
parse var
src/HOL/Types_To_Sets/unoverload_type.ML
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:37:47 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:11:35 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 -> string -> thm -> thm
     1.8 -  val unoverload_type_attr: string -> attribute
     1.9 +  val unoverload_type: Context.generic -> indexname -> thm -> thm
    1.10 +  val unoverload_type_attr: indexname -> attribute
    1.11  end;
    1.12  
    1.13  structure Unoverload_Type : UNOVERLOAD_TYPE =
    1.14 @@ -39,13 +39,13 @@
    1.15      (tvar, thm')
    1.16    end
    1.17  
    1.18 -fun unoverload_type context s thm =
    1.19 +fun unoverload_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    in
    1.24 -  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
    1.25 -    raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
    1.26 +  case find_first (fn (y, _) => x = y) tvars of NONE =>
    1.27 +    raise THM ("unoverload_type: type variable ("^(@{make_string} x)^") not in theorem", 0, [thm])
    1.28    | SOME (x as (_, sort)) =>
    1.29      let
    1.30        val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
    1.31 @@ -56,13 +56,9 @@
    1.32      end
    1.33    end
    1.34  
    1.35 -val tyN = (Args.context -- Args.typ) >>
    1.36 -  (fn (_, TFree (n, _)) => n
    1.37 -  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
    1.38 -
    1.39 -fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
    1.40 +fun unoverload_type_attr x = Thm.rule_attribute [] (fn context => unoverload_type context x)
    1.41  
    1.42  val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
    1.43 -  (tyN >> unoverload_type_attr) "internalize a sort"))
    1.44 +  (Scan.lift Args.var >> unoverload_type_attr) "internalize a sort"))
    1.45  
    1.46  end
    1.47 \ No newline at end of file