TFL/dcterm.ML
changeset 15674 4a1d07bb53e2
parent 15531 08c8dad8e399
child 22591 7d1015d59f24
equal deleted inserted replaced
15673:60c56561bcf4 15674:4a1d07bb53e2
    69 fun cabs a t = Thm.cabs a t
    69 fun cabs a t = Thm.cabs a t
    70   handle CTERM msg => raise ERR "cabs" msg;
    70   handle CTERM msg => raise ERR "cabs" msg;
    71 
    71 
    72 
    72 
    73 (*---------------------------------------------------------------------------
    73 (*---------------------------------------------------------------------------
    74  * SOME simple constructor functions.
    74  * Some simple constructor functions.
    75  *---------------------------------------------------------------------------*)
    75  *---------------------------------------------------------------------------*)
    76 
    76 
    77 val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;
    77 val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;
    78 
    78 
    79 fun mk_exists (r as (Bvar, Body)) =
    79 fun mk_exists (r as (Bvar, Body)) =