src/HOL/Tools/Nitpick/nitpick.ML
changeset 34123 c4988215a691
parent 34121 5e831d805118
child 34124 c4628a1dcf75
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 14 12:31:00 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 14 16:48:49 2009 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4    | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
     1.5  
     1.6  (* ('a * bool option) list -> bool *)
     1.7 -fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
     1.8 +fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
     1.9  
    1.10  val syntactic_sorts =
    1.11    @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
    1.12 @@ -413,9 +413,9 @@
    1.13                                         string_of_int j0))
    1.14                           (Typtab.dest ofs)
    1.15  *)
    1.16 -        val all_precise = forall (is_precise_type datatypes) Ts
    1.17 +        val all_exact = forall (is_exact_type datatypes) Ts
    1.18          (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
    1.19 -        val repify_consts = choose_reps_for_consts scope all_precise
    1.20 +        val repify_consts = choose_reps_for_consts scope all_exact
    1.21          val main_j0 = offset_of_type ofs bool_T
    1.22          val (nat_card, nat_j0) = spec_of_type scope nat_T
    1.23          val (int_card, int_j0) = spec_of_type scope int_T