src/HOLCF/Tools/domain/domain_extender.ML
changeset 31229 8a890890d143
parent 31228 bcacfd816d28
child 31288 67dff9c5b2bd
equal deleted inserted replaced
31228:bcacfd816d28 31229:8a890890d143
   121       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
   121       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
   122       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
   122       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
   123     fun one_con (con,args,mx) =
   123     fun one_con (con,args,mx) =
   124 	((Syntax.const_name mx (Binding.name_of con)),
   124 	((Syntax.const_name mx (Binding.name_of con)),
   125 	 ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
   125 	 ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
   126 					find_index_eq tp dts,
       
   127 					DatatypeAux.dtyp_of_typ new_dts tp),
   126 					DatatypeAux.dtyp_of_typ new_dts tp),
   128 					Option.map Binding.name_of sel,vn))
   127 					Option.map Binding.name_of sel,vn))
   129 	     (args,(mk_var_names(map (typid o third) args)))
   128 	     (args,(mk_var_names(map (typid o third) args)))
   130 	 ) : cons;
   129 	 ) : cons;
   131     val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
   130     val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;