src/HOL/Tools/TFL/rules.ML
changeset 38801 319a28dd3564
parent 38554 f8999e19dd49
child 41164 6854e9a40edc
--- 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)