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 453e0c833a5859a01020060307df62b9cfebde78..6df44f117225864244400300460dc54c11e3123d 100644 --- a/de.prob.core/src/de/prob/eventb/translator/Theories.java +++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java @@ -322,7 +322,7 @@ public class Theories { throws CoreException { prologOutput.openTerm("operator"); - prologOutput.printAtom(opDef.getLabel()); + prologOutput.printAtom(opDef.getLabel()); // Name of the operator final FormulaFactory ff = theory.getFormulaFactory(); final ITypeEnvironment teFromFF = theory.getTypeEnvironment(ff); @@ -337,6 +337,9 @@ public class Theories { } // WD Condition + // TODO: does not seem to get the user-defined WD conditions + // we should probably call in INewOperatorDefinition.java : IOperatorWDCondition[] getOperatorWDConditions() throws RodinDBException; + // and convert this to a Predicate Predicate wdCondition = opDef.getWDCondition(ff, te); printPredicate(prologOutput, wdCondition);