removed separate record_quick_and_dirty_sensitive;
authorwenzelm
Sat, 17 Oct 2009 20:37:38 +0200
changeset 32976 38364667c773
parent 32975 84d105ad5adb
child 32977 d83b9ad78d4b
removed separate record_quick_and_dirty_sensitive;
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