src/HOL/Tools/specification_package.ML
changeset 14117 d3512dedbaea
parent 14116 63337d8e6e0f
child 14118 05416ba8eef2
equal deleted inserted replaced
14116:63337d8e6e0f 14117:d3512dedbaea
    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