changed comment for const_name
authorclasohm
Wed, 06 Jul 1994 11:53:30 +0200
changeset 448 d7ff85d292c7
parent 447 d1f827fa0a18
child 449 75ac32497f09
changed comment for const_name
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];