# HG changeset patch
# User clasohm
# Date 773488410 -7200
# Node ID d7ff85d292c7ef19698b2d2c5b49e1cf03de4899
# Parent  d1f827fa0a18970f3e3997143df5badfb961e330
changed comment for const_name

diff -r d1f827fa0a18 -r d7ff85d292c7 src/ZF/constructor.ML
--- a/src/ZF/constructor.ML	Wed Jul 06 11:36:00 1994 +0200
+++ b/src/ZF/constructor.ML	Wed Jul 06 11:53:30 1994 +0200
@@ -69,10 +69,12 @@
 
 (*Constructors with types and arguments*)
 fun mk_con_ty_list cons_pairs = 
-  let fun mk_con_ty (a, st, syn) =
+  let fun mk_con_ty (id, st, syn) =
 	  let val T = rdty st;
 	      val args = mk_frees "xa" (binder_types T);
-              val name = const_name a syn; (* adds "op" to infix constructors*)
+              val name = const_name id syn;
+                            (* because of mixfix annotations the internal name 
+                               can be different from 'id' *)
 	  in (name, T, args) end;
 
       fun pairtypes c = flatten_consts [c];