34 val live = live_of_bnf (hd bnfs); |
34 val live = live_of_bnf (hd bnfs); |
35 val n = length bnfs; (*active*) |
35 val n = length bnfs; (*active*) |
36 val ks = 1 upto n; |
36 val ks = 1 upto n; |
37 val m = live - n; (*passive, if 0 don't generate a new BNF*) |
37 val m = live - n; (*passive, if 0 don't generate a new BNF*) |
38 |
38 |
39 val note_all = Config.get lthy bnf_note_all; |
39 val internals = Config.get lthy bnf_internals; |
40 val b_names = map Binding.name_of bs; |
40 val b_names = map Binding.name_of bs; |
41 val b_name = mk_common_name b_names; |
41 val b_name = mk_common_name b_names; |
42 val b = Binding.name b_name; |
42 val b = Binding.name b_name; |
43 |
43 |
44 fun mk_internal_of_b name = |
44 fun mk_internal_of_b name = |
45 Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed; |
45 Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed; |
46 fun mk_internal_b name = mk_internal_of_b name b; |
46 fun mk_internal_b name = mk_internal_of_b name b; |
47 fun mk_internal_bs name = map (mk_internal_of_b name) bs; |
47 fun mk_internal_bs name = map (mk_internal_of_b name) bs; |
48 val external_bs = map2 (Binding.prefix false) b_names bs |
48 val external_bs = map2 (Binding.prefix false) b_names bs |
49 |> not note_all ? map Binding.concealed; |
49 |> not internals ? map Binding.concealed; |
50 |
50 |
51 val deads = fold (union (op =)) Dss resDs; |
51 val deads = fold (union (op =)) Dss resDs; |
52 val names_lthy = fold Variable.declare_typ deads lthy; |
52 val names_lthy = fold Variable.declare_typ deads lthy; |
53 val passives = map fst (subtract (op = o apsnd TFree) deads resBs); |
53 val passives = map fst (subtract (op = o apsnd TFree) deads resBs); |
54 |
54 |
1938 |> maps (fn (thmN, thmss) => |
1938 |> maps (fn (thmN, thmss) => |
1939 map2 (fn b => fn thms => |
1939 map2 (fn b => fn thms => |
1940 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1940 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1941 bs thmss); |
1941 bs thmss); |
1942 |
1942 |
1943 val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes); |
1943 val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes); |
1944 |
1944 |
1945 val fp_res = |
1945 val fp_res = |
1946 {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, |
1946 {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, |
1947 xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1947 xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1948 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, |
1948 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, |