src/Pure/Isar/class_target.ML
changeset 31210 d6681ddc046c
parent 31012 751f5aa3e315
child 31214 b67179528acd
equal deleted inserted replaced
31209:77da3aad5917 31210:d6681ddc046c
   439 (* syntax *)
   439 (* syntax *)
   440 
   440 
   441 fun synchronize_inst_syntax ctxt =
   441 fun synchronize_inst_syntax ctxt =
   442   let
   442   let
   443     val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
   443     val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
   444     val thy = ProofContext.theory_of ctxt;
   444     val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
   445     fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   445     fun subst (c, ty) = case inst_tyco_of (c, ty)
   446          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   446          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   447              of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   447              of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   448               | NONE => NONE)
   448               | NONE => NONE)
   449           | NONE => NONE;
   449           | NONE => NONE;
   450     val unchecks =
   450     val unchecks =
   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     fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   515     val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of thy);
       
   516     val typ_instance = Type.typ_instance (Sign.tsig_of thy);
       
   517     fun improve (c, ty) = case inst_tyco_of (c, ty)
   516      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   518      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   517          of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
   519          of SOME (_, ty') => if typ_instance (ty', ty)
   518               then SOME (ty, ty') else NONE
   520               then SOME (ty, ty') else NONE
   519           | NONE => NONE)
   521           | NONE => NONE)
   520       | NONE => NONE;
   522       | NONE => NONE;
   521   in
   523   in
   522     thy
   524     thy