src/Pure/Isar/class_target.ML
changeset 31210 d6681ddc046c
parent 31012 751f5aa3e315
child 31214 b67179528acd
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed May 20 10:37:38 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed May 20 12:09:07 2009 +0200
     1.3 @@ -441,8 +441,8 @@
     1.4  fun synchronize_inst_syntax ctxt =
     1.5    let
     1.6      val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
     1.7 -    val thy = ProofContext.theory_of ctxt;
     1.8 -    fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
     1.9 +    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
    1.10 +    fun subst (c, ty) = case inst_tyco_of (c, ty)
    1.11           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.12               of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.13                | NONE => NONE)
    1.14 @@ -512,9 +512,11 @@
    1.15      fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
    1.16       of NONE => NONE
    1.17        | SOME ts' => SOME (ts', ctxt);
    1.18 -    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.19 +    val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of thy);
    1.20 +    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
    1.21 +    fun improve (c, ty) = case inst_tyco_of (c, ty)
    1.22       of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
    1.23 -         of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
    1.24 +         of SOME (_, ty') => if typ_instance (ty', ty)
    1.25                then SOME (ty, ty') else NONE
    1.26            | NONE => NONE)
    1.27        | NONE => NONE;