# HG changeset patch
# User wenzelm
# Date 1187293927 -7200
# Node ID 229fdfc1ddd97bec70a31d79bf5645c65746cfbf
# Parent  a50cdc42798d84db549184fe835d2480881fce4a
removed dead code;

diff -r a50cdc42798d -r 229fdfc1ddd9 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 16 18:53:22 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 16 21:52:07 2007 +0200
@@ -512,14 +512,13 @@
 fun integer_nnf_conv ctxt env =
  nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
 
-(* val my_term = ref (@{cterm "NotaHING"}); *)
 local
  val pcv = Simplifier.rewrite 
      (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) 
                       @ [not_all,all_not_ex, ex_disj_distrib]))
  val postcv = Simplifier.rewrite presburger_ss
  fun conv ctxt p = 
-  let val _ = () (* my_term := p *)
+  let val _ = ()
   in
    Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
       (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)