equal
deleted
inserted
replaced
76 (*Now we know they are all Consts, so get their names, type and params*) |
76 (*Now we know they are all Consts, so get their names, type and params*) |
77 val rec_names = map (#1 o dest_Const) rec_hds |
77 val rec_names = map (#1 o dest_Const) rec_hds |
78 and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); |
78 and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); |
79 |
79 |
80 val rec_base_names = map Long_Name.base_name rec_names; |
80 val rec_base_names = map Long_Name.base_name rec_names; |
81 val dummy = assert_all Syntax.is_identifier rec_base_names |
81 val dummy = assert_all Lexicon.is_identifier rec_base_names |
82 (fn a => "Base name of recursive set not an identifier: " ^ a); |
82 (fn a => "Base name of recursive set not an identifier: " ^ a); |
83 |
83 |
84 local (*Checking the introduction rules*) |
84 local (*Checking the introduction rules*) |
85 val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms; |
85 val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms; |
86 fun intr_ok set = |
86 fun intr_ok set = |