Nominal/NewFv.thy
changeset 2163 5dc48e1af733
parent 2146 a2f70c09e77d
child 2213 231a20534950
child 2288 3b83960f9544
equal deleted inserted replaced
2156:029f8aabed12 2163:5dc48e1af733
   288 in
   288 in
   289   (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
   289   (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
   290 end
   290 end
   291 *}
   291 *}
   292 
   292 
   293 end
   293 (**************************************************)
       
   294 
       
   295 datatype foo =
       
   296   C1 nat
       
   297 | C2 foo int
       
   298 
       
   299 (*
       
   300 ML {* 
       
   301 fun mk_body descr sorts fv_ty_map dtyp =
       
   302 let
       
   303   val nth_dtyp_constr_tys descr sorts
       
   304 in
       
   305   true
       
   306 end
       
   307 *}
       
   308 *)
       
   309 
       
   310 end