566 val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names'; |
566 val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names'; |
567 |
567 |
568 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) = |
568 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) = |
569 thy3 |
569 thy3 |
570 |> Sign.map_naming Name_Space.conceal |
570 |> Sign.map_naming Name_Space.conceal |
571 |> Inductive.add_inductive_global (serial ()) |
571 |> Inductive.add_inductive_global |
572 {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name, |
572 {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name, |
573 coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} |
573 coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} |
574 (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) |
574 (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) |
575 (rep_set_names' ~~ recTs')) |
575 (rep_set_names' ~~ recTs')) |
576 [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] |
576 [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] |
1509 ([], [], [], [], 0); |
1509 ([], [], [], [], 0); |
1510 |
1510 |
1511 val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = |
1511 val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = |
1512 thy10 |
1512 thy10 |
1513 |> Sign.map_naming Name_Space.conceal |
1513 |> Sign.map_naming Name_Space.conceal |
1514 |> Inductive.add_inductive_global (serial ()) |
1514 |> Inductive.add_inductive_global |
1515 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, |
1515 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, |
1516 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
1516 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
1517 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
1517 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
1518 (map dest_Free rec_fns) |
1518 (map dest_Free rec_fns) |
1519 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] |
1519 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] |