Changed cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind definition

diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml
index 9384b8430537108af8476045f9dc4abfba5da0d7..f1e888d98d9c2c2308629cc1c52f70652f3b51a3 100644 (file)
--- a/helm/meta_style/set.xml
+++ b/helm/meta_style/set.xml
@@ -28,24 +28,23 @@
        </mapp>
 </NotOperator>
 
-<Operator
+<OpSet
  name  = "EMPTY SET"
  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
  cook  = "true">
-       <mop tag="set" helm:xref="$APP-ID"/>
-</Operator>
-
-<Operator
- name  = "EMPTY SET"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
- cook  = "true"
- arity = "1">
-       <mapp>
-               <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
-               <param id="1"/>
+       
+       <Case arity="0">
                <mop tag="set" helm:xref="$APP-ID"/>
-       </mapp>
-</Operator>
+       </Case>
+
+       <Case arity="1">
+               <mapp>
+                       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+                       <param id="1"/>
+                       <mop tag="set" helm:xref="$APP-ID"/>
+               </mapp>
+       </Case>
+</OpSet>
 
 <OpSet
  name  = "SINGLETON"