src/Pure/Isar/class_target.ML
changeset 33969 1e7ca47c6c3d
parent 33967 e191b400a8e0
child 35021 c839a4c670c6
     1.1 --- a/src/Pure/Isar/class_target.ML	Mon Nov 30 11:42:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon Nov 30 12:28:12 2009 +0100
     1.3 @@ -278,7 +278,7 @@
     1.4      fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
     1.5       of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
     1.6           of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
     1.7 -             of SOME (_, ty' as TVar (tvar as (vi, sort))) =>
     1.8 +             of SOME (_, ty' as TVar (vi, sort)) =>
     1.9                    if TypeInfer.is_param vi
    1.10                      andalso Sorts.sort_le algebra (base_sort, sort)
    1.11                        then SOME (ty', TFree (Name.aT, base_sort))
    1.12 @@ -434,9 +434,10 @@
    1.13  
    1.14  fun synchronize_inst_syntax ctxt =
    1.15    let
    1.16 -    val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
    1.17 +    val Instantiation { params, ... } = Instantiation.get ctxt;
    1.18  
    1.19 -    val lookup_inst_param = AxClass.lookup_inst_param (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    1.20 +    val lookup_inst_param = AxClass.lookup_inst_param
    1.21 +      (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    1.22      fun subst (c, ty) = case lookup_inst_param (c, ty)
    1.23       of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.24        | NONE => NONE;
    1.25 @@ -563,8 +564,7 @@
    1.26  
    1.27  fun conclude_instantiation lthy =
    1.28    let
    1.29 -    val { arities, params } = the_instantiation lthy;
    1.30 -    val (tycos, vs, sort) = arities;
    1.31 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    1.32      val thy = ProofContext.theory_of lthy;
    1.33      val _ = map (fn tyco => if Sign.of_sort thy
    1.34          (Type (tyco, map TFree vs), sort)
    1.35 @@ -574,8 +574,7 @@
    1.36  
    1.37  fun pretty_instantiation lthy =
    1.38    let
    1.39 -    val { arities, params } = the_instantiation lthy;
    1.40 -    val (tycos, vs, sort) = arities;
    1.41 +    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
    1.42      val thy = ProofContext.theory_of lthy;
    1.43      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    1.44      fun pr_param ((c, _), (v, ty)) =