equal
deleted
inserted
replaced
70 val cname_full = Sign.intern_const (sign_of thy) cname |
70 val cname_full = Sign.intern_const (sign_of thy) cname |
71 val cdefname = if thname = "" |
71 val cdefname = if thname = "" |
72 then Thm.def_name (Sign.base_name cname) |
72 then Thm.def_name (Sign.base_name cname) |
73 else thname |
73 else thname |
74 val co = Const(cname_full,ctype) |
74 val co = Const(cname_full,ctype) |
75 val def = Logic.mk_implies(HOLogic.mk_Trueprop HOLogic.false_const, |
75 val thy' = Theory.add_finals_i covld [co] thy |
76 Logic.mk_equals (co,choice_const ctype $ P)) |
|
77 val (thy',_) = PureThy.add_defs_i covld [((cdefname,def),[])] thy |
|
78 val tm' = case P of |
76 val tm' = case P of |
79 Abs(_, _, bodt) => subst_bound (co, bodt) |
77 Abs(_, _, bodt) => subst_bound (co, bodt) |
80 | _ => P $ co |
78 | _ => P $ co |
81 in |
79 in |
82 process cos (thy',tm') |
80 process cos (thy',tm') |