src/HOL/Tools/datatype_abs_proofs.ML
changeset 24423 ae9cd0e92423
parent 24346 4f6b71b84ee7
child 24589 d3fca349736c
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -429,6 +429,7 @@
     1.4          thy
     1.5          |> Class.prove_instance_arity (Class.intro_classes_tac [])
     1.6              [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
     1.7 +        |> snd
     1.8        end
     1.9  
    1.10      val (size_def_thms, thy') =