equal
deleted
inserted
replaced
69 |
69 |
70 fun add_const_def s th name_opt thy = |
70 fun add_const_def s th name_opt thy = |
71 let |
71 let |
72 val th = Thm.legacy_freezeT th |
72 val th = Thm.legacy_freezeT th |
73 val name = case name_opt of |
73 val name = case name_opt of |
74 NONE => (fst o dest_Const o fst o HOLogic.dest_eq o |
74 NONE => dest_Const_name (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th)))) |
75 HOLogic.dest_Trueprop o Thm.prop_of) th |
|
76 | SOME n => n |
75 | SOME n => n |
77 val thy' = add_const_map s name thy |
76 val thy' = add_const_map s name thy |
78 in |
77 in |
79 Data.map (fn {const_map, ty_map, const_def, ty_def} => |
78 Data.map (fn {const_map, ty_map, const_def, ty_def} => |
80 {const_map = const_map, ty_map = ty_map, |
79 {const_map = const_map, ty_map = ty_map, |
85 let |
84 let |
86 val th = Thm.legacy_freezeT th |
85 val th = Thm.legacy_freezeT th |
87 val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th)) |
86 val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th)) |
88 val (l, abst) = dest_comb l |
87 val (l, abst) = dest_comb l |
89 val (_, rept) = dest_comb l |
88 val (_, rept) = dest_comb l |
90 val (absn, _) = dest_Const abst |
89 val absn = dest_Const_name abst |
91 val (repn, _) = dest_Const rept |
90 val repn = dest_Const_name rept |
92 val nty = domain_type (fastype_of rept) |
91 val nty = domain_type (fastype_of rept) |
93 val ntyn = dest_Type_name nty |
92 val ntyn = dest_Type_name nty |
94 val thy2 = add_typ_map tyname ntyn thy |
93 val thy2 = add_typ_map tyname ntyn thy |
95 val thy3 = add_const_map absname absn thy2 |
94 val thy3 = add_const_map absname absn thy2 |
96 val thy4 = add_const_map repname repn thy3 |
95 val thy4 = add_const_map repname repn thy3 |