55 val Suml_name = "Datatype.Suml"; |
55 val Suml_name = "Datatype.Suml"; |
56 val Sumr_name = "Datatype.Sumr"; |
56 val Sumr_name = "Datatype.Sumr"; |
57 |
57 |
58 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
58 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
59 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
59 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
60 Lim_inject, Suml_inject, Sumr_inject] = |
60 Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy) |
61 map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE))) |
61 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
62 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
62 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
63 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
63 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
64 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
|
65 |
64 |
66 val descr' = List.concat descr; |
65 val descr' = List.concat descr; |
67 |
66 |
68 val big_name = space_implode "_" new_type_names; |
67 val big_name = space_implode "_" new_type_names; |
69 val thy1 = add_path flat_names big_name thy; |
68 val thy1 = add_path flat_names big_name thy; |