removed dead code;
authorwenzelm
Thu Aug 16 21:52:07 2007 +0200 (2007-08-16)
changeset 24298229fdfc1ddd9
parent 24297 a50cdc42798d
child 24299 91d893799212
removed dead code;
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 16 18:53:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 16 21:52:07 2007 +0200
     1.3 @@ -512,14 +512,13 @@
     1.4  fun integer_nnf_conv ctxt env =
     1.5   nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
     1.6  
     1.7 -(* val my_term = ref (@{cterm "NotaHING"}); *)
     1.8  local
     1.9   val pcv = Simplifier.rewrite 
    1.10       (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) 
    1.11                        @ [not_all,all_not_ex, ex_disj_distrib]))
    1.12   val postcv = Simplifier.rewrite presburger_ss
    1.13   fun conv ctxt p = 
    1.14 -  let val _ = () (* my_term := p *)
    1.15 +  let val _ = ()
    1.16    in
    1.17     Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
    1.18        (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)