43 |
43 |
44 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) |
44 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) |
45 new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = |
45 new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = |
46 let |
46 let |
47 val Datatype_thy = theory "Datatype"; |
47 val Datatype_thy = theory "Datatype"; |
48 val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node"; |
48 val node_name = "Datatype_Universe.node"; |
49 val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name, |
49 val In0_name = "Datatype_Universe.In0"; |
50 Funs_name, o_name, sum_case_name] = |
50 val In1_name = "Datatype_Universe.In1"; |
51 map (Sign.intern_const (Theory.sign_of Datatype_thy)) |
51 val Scons_name = "Datatype_Universe.Scons"; |
52 ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"]; |
52 val Leaf_name = "Datatype_Universe.Leaf"; |
|
53 val Numb_name = "Datatype_Universe.Numb"; |
|
54 val Lim_name = "Datatype_Universe.Lim"; |
|
55 val Funs_name = "Datatype_Universe.Funs"; |
|
56 val o_name = "Fun.op o"; |
|
57 val sum_case_name = "Datatype.sum.sum_case"; |
53 |
58 |
54 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq, |
59 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq, |
55 In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject, |
60 In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject, |
56 Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy) |
61 Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy) |
57 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq", |
62 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq", |