equal
deleted
inserted
replaced
326 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
326 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
327 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
327 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
328 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
328 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
329 (add_binds alpha_eqs) [] lthy'') |
329 (add_binds alpha_eqs) [] lthy'') |
330 in |
330 in |
331 ((fvs, alphas), lthy'') |
331 ((fvs, alphas), lthy''') |
332 end |
332 end |
333 *} |
333 *} |
334 |
334 |
335 (* |
335 (* |
336 atom_decl name |
336 atom_decl name |