src/Pure/Isar/class.ML
changeset 26939 1035c89b4c02
parent 26761 190da765a628
child 26995 2511a72dd73c
equal deleted inserted replaced
26938:64e850c3da9e 26939:1035c89b4c02
   720       then NONE else SOME ((c, tyco),
   720       then NONE else SOME ((c, tyco),
   721         (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   721         (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   722     val inst_params = map_product get_param tycos params |> map_filter I;
   722     val inst_params = map_product get_param tycos params |> map_filter I;
   723     val primary_constraints = map (apsnd
   723     val primary_constraints = map (apsnd
   724       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
   724       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
   725     val pp = Sign.pp thy;
   725     val pp = Syntax.pp_global thy;
   726     val algebra = Sign.classes_of thy
   726     val algebra = Sign.classes_of thy
   727       |> fold (fn tyco => Sorts.add_arities pp
   727       |> fold (fn tyco => Sorts.add_arities pp
   728             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   728             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   729     val consts = Sign.consts_of thy;
   729     val consts = Sign.consts_of thy;
   730     val improve_constraints = AList.lookup (op =)
   730     val improve_constraints = AList.lookup (op =)
   791     val (tycos, vs, sort) = arities;
   791     val (tycos, vs, sort) = arities;
   792     val thy = ProofContext.theory_of lthy;
   792     val thy = ProofContext.theory_of lthy;
   793     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   793     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   794     fun pr_param ((c, _), (v, ty)) =
   794     fun pr_param ((c, _), (v, ty)) =
   795       (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   795       (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   796         (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Sign.pretty_typ thy ty];
   796         (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   797   in
   797   in
   798     (Pretty.block o Pretty.fbreaks)
   798     (Pretty.block o Pretty.fbreaks)
   799       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   799       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   800   end;
   800   end;
   801 
   801