# HG changeset patch
# User wenzelm
# Date 1255804658 -7200
# Node ID 38364667c7731bf7fd13f287f67d0f4ed4548114
# Parent  84d105ad5adb9c2c8cf902dc016c05ab4b17b4f2
removed separate record_quick_and_dirty_sensitive;

diff -r 84d105ad5adb -r 38364667c773 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Oct 17 20:15:59 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sat Oct 17 20:37:38 2009 +0200
@@ -26,7 +26,6 @@
 sig
   include BASIC_RECORD
   val timing: bool Unsynchronized.ref
-  val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
   val updateN: string
   val ext_typeN: string
   val extN: string
@@ -1011,11 +1010,8 @@
 
 (** record simprocs **)
 
-val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
-
-
 fun quick_and_dirty_prove stndrd thy asms prop tac =
-  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
+  if ! quick_and_dirty then
     Goal.prove (ProofContext.init thy) [] []
       (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
       (K (Skip_Proof.cheat_tac @{theory HOL}))
@@ -1026,9 +1022,7 @@
     in if stndrd then Drule.standard prf else prf end;
 
 fun quick_and_dirty_prf noopt opt () =
-  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
-  then noopt ()
-  else opt ();
+  if ! quick_and_dirty then noopt () else opt ();
 
 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   (case get_updates thy u of