TFL/dcterm.ML
changeset 22591 7d1015d59f24
parent 15674 4a1d07bb53e2
child 22596 d0d2af4db18f
equal deleted inserted replaced
22590:ac84debdd7d3 22591:7d1015d59f24
    56 
    56 
    57 fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
    57 fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
    58 
    58 
    59 
    59 
    60 fun dest_comb t = Thm.dest_comb t
    60 fun dest_comb t = Thm.dest_comb t
    61   handle CTERM msg => raise ERR "dest_comb" msg;
    61   handle CTERM (msg, _) => raise ERR "dest_comb" msg;
    62 
    62 
    63 fun dest_abs a t = Thm.dest_abs a t
    63 fun dest_abs a t = Thm.dest_abs a t
    64   handle CTERM msg => raise ERR "dest_abs" msg;
    64   handle CTERM (msg, _) => raise ERR "dest_abs" msg;
    65 
    65 
    66 fun capply t u = Thm.capply t u
    66 fun capply t u = Thm.capply t u
    67   handle CTERM msg => raise ERR "capply" msg;
    67   handle CTERM (msg, _) => raise ERR "capply" msg;
    68 
    68 
    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 HOL.thy o Const;
    78 
    78 
    79 fun mk_exists (r as (Bvar, Body)) =
    79 fun mk_exists (r as (Bvar, Body)) =
    80   let val ty = #T(rep_cterm Bvar)
    80   let val ty = #T(rep_cterm Bvar)
    81       val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    81       val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    82   in capply c (uncurry cabs r) end;
    82   in capply c (uncurry cabs r) end;