src/HOL/Tools/res_axioms.ML
changeset 32740 9dd0a2f83429
parent 32283 3bebc195c124
child 32955 4a78daeb012b
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -16,7 +16,8 @@
     1.4    val combinators: thm -> thm
     1.5    val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
     1.6    val atpset_rules_of: Proof.context -> (string * thm) list
     1.7 -  val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
     1.8 +  val suppress_endtheory: bool Unsynchronized.ref
     1.9 +    (*for emergency use where endtheory causes problems*)
    1.10    val setup: theory -> theory
    1.11  end;
    1.12  
    1.13 @@ -66,11 +67,11 @@
    1.14    prefix for the Skolem constant.*)
    1.15  fun declare_skofuns s th =
    1.16    let
    1.17 -    val nref = ref 0
    1.18 +    val nref = Unsynchronized.ref 0
    1.19      fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
    1.20            (*Existential: declare a Skolem function, then insert into body and continue*)
    1.21            let
    1.22 -            val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
    1.23 +            val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
    1.24              val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
    1.25              val Ts = map type_of args0
    1.26              val extraTs = rhs_extra_types (Ts ---> T) xtp
    1.27 @@ -97,14 +98,14 @@
    1.28  
    1.29  (*Traverse a theorem, accumulating Skolem function definitions.*)
    1.30  fun assume_skofuns s th =
    1.31 -  let val sko_count = ref 0
    1.32 +  let val sko_count = Unsynchronized.ref 0
    1.33        fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
    1.34              (*Existential: declare a Skolem function, then insert into body and continue*)
    1.35              let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
    1.36                  val args = OldTerm.term_frees xtp \\ skos  (*the formal parameters*)
    1.37                  val Ts = map type_of args
    1.38                  val cT = Ts ---> T
    1.39 -                val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
    1.40 +                val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
    1.41                  val c = Free (id, cT)
    1.42                  val rhs = list_abs_free (map dest_Free args,
    1.43                                           HOLogic.choice_const T $ xtp)
    1.44 @@ -449,7 +450,7 @@
    1.45  
    1.46  end;
    1.47  
    1.48 -val suppress_endtheory = ref false;
    1.49 +val suppress_endtheory = Unsynchronized.ref false;
    1.50  
    1.51  fun clause_cache_endtheory thy =
    1.52    if ! suppress_endtheory then NONE