removed separate record_quick_and_dirty_sensitive;
authorwenzelm
Sat Oct 17 20:37:38 2009 +0200 (2009-10-17)
changeset 3297638364667c773
parent 32975 84d105ad5adb
child 32977 d83b9ad78d4b
removed separate record_quick_and_dirty_sensitive;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 20:15:59 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 20:37:38 2009 +0200
     1.3 @@ -26,7 +26,6 @@
     1.4  sig
     1.5    include BASIC_RECORD
     1.6    val timing: bool Unsynchronized.ref
     1.7 -  val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
     1.8    val updateN: string
     1.9    val ext_typeN: string
    1.10    val extN: string
    1.11 @@ -1011,11 +1010,8 @@
    1.12  
    1.13  (** record simprocs **)
    1.14  
    1.15 -val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
    1.16 -
    1.17 -
    1.18  fun quick_and_dirty_prove stndrd thy asms prop tac =
    1.19 -  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
    1.20 +  if ! quick_and_dirty then
    1.21      Goal.prove (ProofContext.init thy) [] []
    1.22        (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
    1.23        (K (Skip_Proof.cheat_tac @{theory HOL}))
    1.24 @@ -1026,9 +1022,7 @@
    1.25      in if stndrd then Drule.standard prf else prf end;
    1.26  
    1.27  fun quick_and_dirty_prf noopt opt () =
    1.28 -  if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
    1.29 -  then noopt ()
    1.30 -  else opt ();
    1.31 +  if ! quick_and_dirty then noopt () else opt ();
    1.32  
    1.33  fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
    1.34    (case get_updates thy u of