41 | proc_exprop ((thname,cname,covld)::cos) (thy,thm) = |
41 | proc_exprop ((thname,cname,covld)::cos) (thy,thm) = |
42 case concl_of thm of |
42 case concl_of thm of |
43 Const("Trueprop",_) $ (Const("Ex",_) $ P) => |
43 Const("Trueprop",_) $ (Const("Ex",_) $ P) => |
44 let |
44 let |
45 val ctype = domain_type (type_of P) |
45 val ctype = domain_type (type_of P) |
|
46 val cname_full = Sign.intern_const (sign_of thy) cname |
46 val cdefname = if thname = "" |
47 val cdefname = if thname = "" |
47 then Thm.def_name (Sign.base_name cname) |
48 then Thm.def_name (Sign.base_name cname) |
48 else thname |
49 else thname |
49 val def_eq = Logic.mk_equals (Const(cname,ctype),choice_const ctype $ P) |
50 val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $ P) |
50 val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy |
51 val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy |
51 val thm' = [thm,hd thms] MRS helper |
52 val thm' = [thm,hd thms] MRS helper |
52 in |
53 in |
53 proc_exprop cos (thy',thm') |
54 proc_exprop cos (thy',thm') |
54 end |
55 end |