1.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Aug 27 15:07:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Aug 27 15:46:08 2010 +0200
     1.3 @@ -46,10 +46,6 @@
     1.4    val simpl_conv: simpset -> thm list -> cterm -> thm
     1.5  
     1.6    val rbeta: thm -> thm
     1.7 -(* For debugging my isabelle solver in the conditional rewriter *)
     1.8 -  val term_ref: term list Unsynchronized.ref
     1.9 -  val thm_ref: thm list Unsynchronized.ref
    1.10 -  val ss_ref: simpset list Unsynchronized.ref
    1.11    val tracing: bool Unsynchronized.ref
    1.12    val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
    1.13                               -> thm -> thm * term list
    1.14 @@ -542,9 +538,6 @@
    1.15  (*---------------------------------------------------------------------------
    1.16   * Trace information for the rewriter
    1.17   *---------------------------------------------------------------------------*)
    1.18 -val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
    1.19 -val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
    1.20 -val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
    1.21  val tracing = Unsynchronized.ref false;
    1.22  
    1.23  fun say s = if !tracing then writeln s else ();
    1.24 @@ -665,9 +658,6 @@
    1.25       val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
    1.26       val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
    1.27       val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
    1.28 -     val dummy = term_ref := []
    1.29 -     val dummy = thm_ref  := []
    1.30 -     val dummy = ss_ref  := []
    1.31       val cut_lemma' = cut_lemma RS eq_reflection
    1.32       fun prover used ss thm =
    1.33       let fun cong_prover ss thm =
    1.34 @@ -676,8 +666,6 @@
    1.35               val dummy = print_thms "cntxt:" cntxt
    1.36               val dummy = say "cong rule:"
    1.37               val dummy = say (Display.string_of_thm_without_context thm)
    1.38 -             val dummy = thm_ref := (thm :: !thm_ref)
    1.39 -             val dummy = ss_ref := (ss :: !ss_ref)
    1.40               (* Unquantified eliminate *)
    1.41               fun uq_eliminate (thm,imp,thy) =
    1.42                   let val tych = cterm_of thy
    1.43 @@ -784,7 +772,6 @@
    1.44                val dummy = tc_list := (TC :: !tc_list)
    1.45                val nestedp = is_some (S.find_term is_func TC)
    1.46                val dummy = if nestedp then say "nested" else say "not_nested"
    1.47 -              val dummy = term_ref := ([func,TC]@(!term_ref))
    1.48                val th' = if nestedp then raise RULES_ERR "solver" "nested function"
    1.49                          else let val cTC = cterm_of thy
    1.50                                                (HOLogic.mk_Trueprop TC)