20 |
20 |
21 (* @chunk make_definitions *) |
21 (* @chunk make_definitions *) |
22 fun make_defs ((binding, syn), trm) lthy = |
22 fun make_defs ((binding, syn), trm) lthy = |
23 let |
23 let |
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
25 val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy |
25 val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy |
26 in |
26 in |
27 (thm, lthy) |
27 (thm, lthy) |
28 end |
28 end |
29 (* @end *) |
29 (* @end *) |
30 |
30 |
178 |
178 |
179 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
179 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
180 val case_names = map (Binding.name_of o fst o fst) specs |
180 val case_names = map (Binding.name_of o fst o fst) specs |
181 in |
181 in |
182 lthy1 |
182 lthy1 |
183 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
183 |> Local_Theory.notes (map (fn (((a, atts), _), th) => |
184 ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
184 ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
185 |-> (fn intross => LocalTheory.note Thm.theoremK |
185 |-> (fn intross => Local_Theory.note |
186 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
186 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
187 |>> snd |
187 |>> snd |
188 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
188 ||>> (Local_Theory.notes (map (fn (((R, _), _), th) => |
189 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
189 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
190 [Attrib.internal (K (Rule_Cases.case_names case_names)), |
190 [Attrib.internal (K (Rule_Cases.case_names case_names)), |
191 Attrib.internal (K (Rule_Cases.consumes 1)), |
191 Attrib.internal (K (Rule_Cases.consumes 1)), |
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
193 (preds ~~ inducts)) #>> maps snd) |
193 (preds ~~ inducts)) #>> maps snd) |