equal
deleted
inserted
replaced
63 val rec_names = map (#1 o dest_Const) rec_hds; |
63 val rec_names = map (#1 o dest_Const) rec_hds; |
64 |
64 |
65 val _ = assert_all Syntax.is_identifier rec_names |
65 val _ = assert_all Syntax.is_identifier rec_names |
66 (fn a => "Name of recursive set not an identifier: " ^ a); |
66 (fn a => "Name of recursive set not an identifier: " ^ a); |
67 |
67 |
68 val _ = assert_all (is_some o lookup_const sign) rec_names |
68 val _ = assert_all (is_some o Sign.const_type sign) rec_names |
69 (fn a => "Recursive set not previously declared as constant: " ^ a); |
69 (fn a => "Recursive set not previously declared as constant: " ^ a); |
70 |
70 |
71 local (*Checking the introduction rules*) |
71 local (*Checking the introduction rules*) |
72 val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; |
72 val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; |
73 fun intr_ok set = |
73 fun intr_ok set = |