diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java
index bb7e443c8e90881027039e22fad11942b1941bc1..6a1629c6374112eddcce24a77454664323c9fc05 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -435,21 +435,19 @@ public class Theories {
 			final IPrologTermOutput pto) throws CoreException {
 		pto.openTerm(functor);
 		pto.printAtom(id.getIdentifierString());
-		//final String typeString = getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE);
-		// todo: is there a better way to check if type refers recursively to def?
-		//if (def.getIdentifierString().equals(typeString)) {
-			// the the checked theory files tcf no longer contain the type paras
+		final String typeString = id.getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE);
+		// todo: is there a better way to check if type refers recursively to def? do we need to trim typeString?
+		// System.out.println("Inductive datatype: " + def.getIdentifierString() + " destructor arg has type: " + typeString);
+		if (def.getIdentifierString().equals(typeString)) {
+			// the checked theory files tcf no longer contain the type paras
 			// the tuf file may contain org.eventb.theory.core.type="Baum(L)"
 			// the tcf file now contains org.eventb.theory.core.type="Baum"
 			// getType would lead to a CoreException
 			// we print the type of the recursive data type directly
-		    // pto.printTypeOfDataType(def,ff,pto);
-		//} else {
-		try {
+		    printTypeOfDataType(def,ff,pto);
+		} else {
 		    Type type = id.getType(ff);
 		    printType(type, pto);
-		} catch (CoreException e) {
-		    printTypeOfDataType(def,ff,pto);
 		}
 		pto.closeTerm();
 	}