# HG changeset patch
# User paulson
# Date 1164972233 -3600
# Node ID 4664489469fc9bda63c5cf1231629afe9d43dbdc
# Parent  296e0c318c3e605337f80b1429bab8f36973e957
Deleted dead code

diff -r 296e0c318c3e -r 4664489469fc src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Fri Dec 01 12:23:39 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Dec 01 12:23:53 2006 +0100
@@ -141,17 +141,6 @@
       lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
   | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
   | to_comb t _ = t;
-    
-(* print a term containing combinators, used for debugging *)
-exception TERM_COMB of term;
-
-fun string_of_term (Const(c,t)) = c
-  | string_of_term (Free(v,t)) = v
-  | string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n)
-  | string_of_term (P $ Q) =
-      "(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" 
-  | string_of_term t =  raise TERM_COMB (t);
-
 
 
 (******************************************************)