src/HOL/Tools/Datatype/datatype_realizer.ML
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 _ = "";