src/Pure/Tools/codegen_data.ML
changeset 21421 3436c269dd23
parent 21338 56d55dd30311
child 21708 45e7491bea47
equal deleted inserted replaced
21420:8b15e5e66813 21421:3436c269dd23
   173           (snd o CodegenConsts.typ_of_inst thy) const;
   173           (snd o CodegenConsts.typ_of_inst thy) const;
   174         val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
   174         val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
   175       in if Sign.typ_equiv thy (ty_decl, ty)
   175       in if Sign.typ_equiv thy (ty_decl, ty)
   176         then SOME (const, thm)
   176         then SOME (const, thm)
   177         else (if is_classop
   177         else (if is_classop
   178             then error
   178             then if !strict_functyp
       
   179               then error
       
   180               else warning #> K NONE
   179           else if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   181           else if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   180             then warning #> (K o SOME) (const, thm)
   182             then warning #> (K o SOME) (const, thm)
   181           else if !strict_functyp
   183           else if !strict_functyp
   182             then error
   184             then error
   183           else warning #> K NONE)
   185           else warning #> K NONE)