src/Pure/Isar/class_target.ML
changeset 31214 b67179528acd
parent 31210 d6681ddc046c
child 31249 d51d2a22a4f9
equal deleted inserted replaced
31213:800787c3210f 31214:b67179528acd
   510     val improve_constraints = AList.lookup (op =)
   510     val improve_constraints = AList.lookup (op =)
   511       (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
   511       (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
   512     fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
   512     fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
   513      of NONE => NONE
   513      of NONE => NONE
   514       | SOME ts' => SOME (ts', ctxt);
   514       | SOME ts' => SOME (ts', ctxt);
   515     val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of thy);
   515     val inst_tyco_of = AxClass.inst_tyco_of consts;
   516     val typ_instance = Type.typ_instance (Sign.tsig_of thy);
   516     val typ_instance = Type.typ_instance (Sign.tsig_of thy);
   517     fun improve (c, ty) = case inst_tyco_of (c, ty)
   517     fun improve (c, ty) = case inst_tyco_of (c, ty)
   518      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   518      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   519          of SOME (_, ty') => if typ_instance (ty', ty)
   519          of SOME (_, ty') => if typ_instance (ty', ty)
   520               then SOME (ty, ty') else NONE
   520               then SOME (ty, ty') else NONE