changeset 40844 | 5895c525739d |
parent 39557 | fe5722fce758 |
child 41423 | 25df154b8ffc |
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Dec 01 15:02:39 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Dec 01 15:03:44 2010 +0100 @@ -25,7 +25,7 @@ fun prf_of thm = Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); -fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT; +fun is_unit t = body_type (fastype_of t) = HOLogic.unitT; fun tname_of (Type (s, _)) = s | tname_of _ = "";