Deleted dead code
authorpaulson
Fri Dec 01 12:23:53 2006 +0100 (2006-12-01)
changeset 216174664489469fc
parent 21616 296e0c318c3e
child 21618 1cbb1134cb6c
Deleted dead code
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Dec 01 12:23:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Dec 01 12:23:53 2006 +0100
     1.3 @@ -141,17 +141,6 @@
     1.4        lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
     1.5    | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
     1.6    | to_comb t _ = t;
     1.7 -    
     1.8 -(* print a term containing combinators, used for debugging *)
     1.9 -exception TERM_COMB of term;
    1.10 -
    1.11 -fun string_of_term (Const(c,t)) = c
    1.12 -  | string_of_term (Free(v,t)) = v
    1.13 -  | string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n)
    1.14 -  | string_of_term (P $ Q) =
    1.15 -      "(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" 
    1.16 -  | string_of_term t =  raise TERM_COMB (t);
    1.17 -
    1.18  
    1.19  
    1.20  (******************************************************)