# HG changeset patch
# User wenzelm
# Date 1175638286 -7200
# Node ID 7d1015d59f24390f3f8ff3579b6fea36fbac7f67
# Parent  ac84debdd7d3fbbca4386f100ef3b267377a3eac
improved exception CTERM;
removed obsolete sign_of/sign_of_thm;

diff -r ac84debdd7d3 -r 7d1015d59f24 TFL/dcterm.ML
--- a/TFL/dcterm.ML	Wed Apr 04 00:11:23 2007 +0200
+++ b/TFL/dcterm.ML	Wed Apr 04 00:11:26 2007 +0200
@@ -58,23 +58,23 @@
 
 
 fun dest_comb t = Thm.dest_comb t
-  handle CTERM msg => raise ERR "dest_comb" msg;
+  handle CTERM (msg, _) => raise ERR "dest_comb" msg;
 
 fun dest_abs a t = Thm.dest_abs a t
-  handle CTERM msg => raise ERR "dest_abs" msg;
+  handle CTERM (msg, _) => raise ERR "dest_abs" msg;
 
 fun capply t u = Thm.capply t u
-  handle CTERM msg => raise ERR "capply" msg;
+  handle CTERM (msg, _) => raise ERR "capply" msg;
 
 fun cabs a t = Thm.cabs a t
-  handle CTERM msg => raise ERR "cabs" msg;
+  handle CTERM (msg, _) => raise ERR "cabs" msg;
 
 
 (*---------------------------------------------------------------------------
  * Some simple constructor functions.
  *---------------------------------------------------------------------------*)
 
-val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;
+val mk_hol_const = Thm.cterm_of HOL.thy o Const;
 
 fun mk_exists (r as (Bvar, Body)) =
   let val ty = #T(rep_cterm Bvar)