src/HOL/Tools/datatype_package.ML
changeset 24346 4f6b71b84ee7
parent 24218 fbf1646b267c
child 24349 0dd8782fb02d
equal deleted inserted replaced
24345:86a3557a9ebb 24346:4f6b71b84ee7
   563     fun instance_size_class tyco thy =
   563     fun instance_size_class tyco thy =
   564       let
   564       let
   565         val n = Sign.arity_number thy tyco;
   565         val n = Sign.arity_number thy tyco;
   566       in
   566       in
   567         thy
   567         thy
   568         |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
   568         |> Class.prove_instance_arity (Class.intro_classes_tac [])
   569              (Class.intro_classes_tac [])
   569             [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
   570       end
   570       end
   571 
   571 
   572     val thy2' = thy
   572     val thy2' = thy
   573 
   573 
   574       (** new types **)
   574       (** new types **)