src/Pure/axclass.ML
changeset 31210 d6681ddc046c
parent 30951 a6e26a248f03
child 31249 d51d2a22a4f9
     1.1 --- a/src/Pure/axclass.ML	Wed May 20 10:37:38 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed May 20 12:09:07 2009 +0200
     1.3 @@ -26,9 +26,9 @@
     1.4    val axiomatize_arity: arity -> theory -> theory
     1.5    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
     1.6    val instance_name: string * class -> string
     1.7 +  val inst_tyco_of: Consts.T -> string * typ -> string option
     1.8    val declare_overloaded: string * typ -> theory -> term * theory
     1.9    val define_overloaded: binding -> string * term -> theory -> thm * theory
    1.10 -  val inst_tyco_of: theory -> string * typ -> string option
    1.11    val unoverload: theory -> thm -> thm
    1.12    val overload: theory -> thm -> thm
    1.13    val unoverload_conv: theory -> conv
    1.14 @@ -249,7 +249,8 @@
    1.15  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    1.16    (get_inst_params thy) [];
    1.17  
    1.18 -fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
    1.19 +fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
    1.20 +val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
    1.21  
    1.22  fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    1.23  fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    1.24 @@ -259,7 +260,7 @@
    1.25  
    1.26  fun unoverload_const thy (c_ty as (c, _)) =
    1.27    case class_of_param thy c
    1.28 -   of SOME class => (case inst_tyco_of thy c_ty
    1.29 +   of SOME class => (case inst_tyco_of' thy c_ty
    1.30         of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    1.31          | NONE => c)
    1.32      | NONE => c;
    1.33 @@ -293,7 +294,7 @@
    1.34      val class = case class_of_param thy c
    1.35       of SOME class => class
    1.36        | NONE => error ("Not a class parameter: " ^ quote c);
    1.37 -    val tyco = case inst_tyco_of thy (c, T)
    1.38 +    val tyco = case inst_tyco_of' thy (c, T)
    1.39       of SOME tyco => tyco
    1.40        | NONE => error ("Illegal type for instantiation of class parameter: "
    1.41          ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    1.42 @@ -318,7 +319,7 @@
    1.43  fun define_overloaded b (c, t) thy =
    1.44    let
    1.45      val T = Term.fastype_of t;
    1.46 -    val SOME tyco = inst_tyco_of thy (c, T);
    1.47 +    val SOME tyco = inst_tyco_of' thy (c, T);
    1.48      val (c', eq) = get_inst_param thy (c, tyco);
    1.49      val prop = Logic.mk_equals (Const (c', T), t);
    1.50      val b' = Thm.def_binding_optional