Nominal/nominal_dt_alpha.ML
changeset 2594 515e5496171c
parent 2593 25dcb2b1329e
child 2611 3d101f2f817c
equal deleted inserted replaced
2593:25dcb2b1329e 2594:515e5496171c
   245 
   245 
   246     val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
   246     val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
   247       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
   247       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
   248     val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
   248     val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
   249 
   249 
   250     val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names))
       
   251 
       
   252     val (alphas, lthy') = Inductive.add_inductive_i
   250     val (alphas, lthy') = Inductive.add_inductive_i
   253        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
   251        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
   254         coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
   252         coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
   255          all_alpha_names [] all_alpha_intros [] lthy
   253          all_alpha_names [] all_alpha_intros [] lthy
   256 
   254