# HG changeset patch
# User wenzelm
# Date 1282916768 -7200
# Node ID 319a28dd3564b60b5817e7f2d6fb76a81aca999d
# Parent  34c84817e39c9255cfc743f574d0567d9508f414
disposed some old debugging tools;

diff -r 34c84817e39c -r 319a28dd3564 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 15:07:35 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 15:46:08 2010 +0200
@@ -164,21 +164,6 @@
   thm list * thm list * thm list -> thm * pss_tree
 type cert_conv = cterm -> thm * pss_tree
 
-val my_eqs = Unsynchronized.ref ([] : thm list);
-val my_les = Unsynchronized.ref ([] : thm list);
-val my_lts = Unsynchronized.ref ([] : thm list);
-val my_proof = Unsynchronized.ref (Axiom_eq 0);
-val my_context = Unsynchronized.ref @{context};
-
-val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
-val my_numeric_eq_conv = Unsynchronized.ref no_conv;
-val my_numeric_ge_conv = Unsynchronized.ref no_conv;
-val my_numeric_gt_conv = Unsynchronized.ref no_conv;
-val my_poly_conv = Unsynchronized.ref no_conv;
-val my_poly_neg_conv = Unsynchronized.ref no_conv;
-val my_poly_add_conv = Unsynchronized.ref no_conv;
-val my_poly_mul_conv = Unsynchronized.ref no_conv;
-
 
     (* Some useful derived rules *)
 fun deduct_antisym_rule tha thb = 
@@ -362,11 +347,6 @@
        poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
        absconv1,absconv2,prover) = 
 let
- val _ = my_context := ctxt 
- val _ = (my_mk_numeric := mk_numeric ; my_numeric_eq_conv := numeric_eq_conv ; 
-          my_numeric_ge_conv := numeric_ge_conv; my_numeric_gt_conv := numeric_gt_conv ;
-          my_poly_conv := poly_conv; my_poly_neg_conv := poly_neg_conv; 
-          my_poly_add_conv := poly_add_conv; my_poly_mul_conv := poly_mul_conv)
  val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
  val prenex_ss = HOL_basic_ss addsimps prenex_simps
  val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
@@ -408,7 +388,6 @@
 
   fun hol_of_positivstellensatz(eqs,les,lts) proof =
    let 
-    val _ = (my_eqs := eqs ; my_les := les ; my_lts := lts ; my_proof := proof)
     fun translate prf = case prf of
         Axiom_eq n => nth eqs n
       | Axiom_le n => nth les n
diff -r 34c84817e39c -r 319a28dd3564 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Aug 27 15:07:35 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Fri Aug 27 15:46:08 2010 +0200
@@ -46,10 +46,6 @@
   val simpl_conv: simpset -> thm list -> cterm -> thm
 
   val rbeta: thm -> thm
-(* For debugging my isabelle solver in the conditional rewriter *)
-  val term_ref: term list Unsynchronized.ref
-  val thm_ref: thm list Unsynchronized.ref
-  val ss_ref: simpset list Unsynchronized.ref
   val tracing: bool Unsynchronized.ref
   val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
                              -> thm -> thm * term list
@@ -542,9 +538,6 @@
 (*---------------------------------------------------------------------------
  * Trace information for the rewriter
  *---------------------------------------------------------------------------*)
-val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
-val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
-val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
 val tracing = Unsynchronized.ref false;
 
 fun say s = if !tracing then writeln s else ();
@@ -665,9 +658,6 @@
      val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
      val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
      val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
-     val dummy = term_ref := []
-     val dummy = thm_ref  := []
-     val dummy = ss_ref  := []
      val cut_lemma' = cut_lemma RS eq_reflection
      fun prover used ss thm =
      let fun cong_prover ss thm =
@@ -676,8 +666,6 @@
              val dummy = print_thms "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (Display.string_of_thm_without_context thm)
-             val dummy = thm_ref := (thm :: !thm_ref)
-             val dummy = ss_ref := (ss :: !ss_ref)
              (* Unquantified eliminate *)
              fun uq_eliminate (thm,imp,thy) =
                  let val tych = cterm_of thy
@@ -784,7 +772,6 @@
               val dummy = tc_list := (TC :: !tc_list)
               val nestedp = is_some (S.find_term is_func TC)
               val dummy = if nestedp then say "nested" else say "not_nested"
-              val dummy = term_ref := ([func,TC]@(!term_ref))
               val th' = if nestedp then raise RULES_ERR "solver" "nested function"
                         else let val cTC = cterm_of thy
                                               (HOLogic.mk_Trueprop TC)