1.1 --- a/NEWS	Tue Jun 01 11:58:50 2010 +0200
     1.2 +++ b/NEWS	Tue Jun 01 12:20:08 2010 +0200
     1.3 @@ -427,6 +427,7 @@
     1.4      record getters.
     1.5    - Fixed soundness bug related to higher-order constructors
     1.6    - Improved precision of set constructs.
     1.7 +  - Added "atoms" option.
     1.8    - Added cache to speed up repeated Kodkod invocations on the same
     1.9      problems.
    1.10    - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and

     2.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Jun 01 11:58:50 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Jun 01 12:20:08 2010 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    * Fixed soundness bug related to higher-order constructors
     2.5    * Improved precision of set constructs
     2.6    * Added cache to speed up repeated Kodkod invocations on the same problems
     2.7 +  * Added "atoms" option
     2.8    * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
     2.9      "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
    2.10    * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 11:58:50 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 12:20:08 2010 +0200
     3.3 @@ -42,6 +42,7 @@
     3.4       show_consts: bool,
     3.5       evals: term list,
     3.6       formats: (term option * int list) list,
     3.7 +     atomss: (typ option * string list) list,
     3.8       max_potential: int,
     3.9       max_genuine: int,
    3.10       check_potential: bool,
    3.11 @@ -112,6 +113,7 @@
    3.12     show_consts: bool,
    3.13     evals: term list,
    3.14     formats: (term option * int list) list,
    3.15 +   atomss: (typ option * string list) list,
    3.16     max_potential: int,
    3.17     max_genuine: int,
    3.18     check_potential: bool,
    3.19 @@ -190,7 +192,7 @@
    3.20           verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
    3.21           destroy_constrs, specialize, star_linear_preds, fast_descrs,
    3.22           peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
    3.23 -         evals, formats, max_potential, max_genuine, check_potential,
    3.24 +         evals, formats, atomss, max_potential, max_genuine, check_potential,
    3.25           check_genuine, batch_size, ...} = params
    3.26      val state_ref = Unsynchronized.ref state
    3.27      val pprint =
    3.28 @@ -575,8 +577,8 @@
    3.29          val (reconstructed_model, codatatypes_ok) =
    3.30            reconstruct_hol_model {show_datatypes = show_datatypes,
    3.31                                   show_consts = show_consts}
    3.32 -              scope formats frees free_names sel_names nonsel_names rel_table
    3.33 -              bounds
    3.34 +              scope formats atomss frees free_names sel_names nonsel_names
    3.35 +              rel_table bounds
    3.36          val genuine_means_genuine =
    3.37            got_all_user_axioms andalso none_true wfs andalso
    3.38            sound_finitizes andalso codatatypes_ok

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 11:58:50 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 12:20:08 2010 +0200
     4.3 @@ -715,7 +715,7 @@
     4.4      val thy = ProofContext.theory_of ctxt
     4.5      val (x as (_, T)) = (s, unarize_unbox_etc_type T)
     4.6    in
     4.7 -    Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
     4.8 +    is_real_constr thy x orelse is_record_constr x orelse
     4.9      (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
    4.10      is_coconstr thy x
    4.11    end
    4.12 @@ -861,9 +861,9 @@
    4.13             let
    4.14               val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
    4.15             in
    4.16 -             map (fn (s', Us) =>
    4.17 -                     (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
    4.18 -                          ---> T)) constrs
    4.19 +             map (apsnd (fn Us =>
    4.20 +                            map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
    4.21 +                 constrs
    4.22             end
    4.23           | NONE =>
    4.24             if is_record_type T then

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Jun 01 11:58:50 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Jun 01 12:20:08 2010 +0200
     5.3 @@ -65,6 +65,7 @@
     5.4     ("show_datatypes", "false"),
     5.5     ("show_consts", "false"),
     5.6     ("format", "1"),
     5.7 +   ("atoms", ""),
     5.8     ("max_potential", "1"),
     5.9     ("max_genuine", "1"),
    5.10     ("check_potential", "false"),
    5.11 @@ -98,10 +99,11 @@
    5.12  fun is_known_raw_param s =
    5.13    AList.defined (op =) default_default_params s orelse
    5.14    AList.defined (op =) negated_params s orelse
    5.15 -  s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse
    5.16 +  member (op =) ["max", "show_all", "eval", "expect"] s orelse
    5.17    exists (fn p => String.isPrefix (p ^ " ") s)
    5.18           ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    5.19 -          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
    5.20 +          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
    5.21 +          "atoms"]
    5.22  
    5.23  fun check_raw_param (s, _) =
    5.24    if is_known_raw_param s then ()
    5.25 @@ -149,8 +151,8 @@
    5.26    let
    5.27      val override_params = maps normalize_raw_param override_params
    5.28      val raw_params = rev override_params @ rev default_params
    5.29 -    val lookup =
    5.30 -      Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
    5.31 +    val raw_lookup = AList.lookup (op =) raw_params
    5.32 +    val lookup = Option.map stringify_raw_param_value o raw_lookup
    5.33      val lookup_string = the_default "" o lookup
    5.34      fun general_lookup_bool option default_value name =
    5.35        case lookup name of
    5.36 @@ -191,27 +193,21 @@
    5.37                       [] => [min_int]
    5.38                     | value => value)
    5.39        | NONE => [min_int]
    5.40 -    fun lookup_ints_assigns read prefix min_int =
    5.41 -      (NONE, lookup_int_seq prefix min_int)
    5.42 +    fun lookup_assigns read prefix default convert =
    5.43 +      (NONE, convert (the_default default (lookup prefix)))
    5.44        :: map (fn (name, value) =>
    5.45                   (SOME (read (String.extract (name, size prefix + 1, NONE))),
    5.46 -                  value |> stringify_raw_param_value
    5.47 -                        |> int_seq_from_string name min_int))
    5.48 +                  convert (stringify_raw_param_value value)))
    5.49               (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
    5.50 +    fun lookup_ints_assigns read prefix min_int =
    5.51 +      lookup_assigns read prefix (signed_string_of_int min_int)
    5.52 +                     (int_seq_from_string prefix min_int)
    5.53      fun lookup_bool_assigns read prefix =
    5.54 -      (NONE, lookup_bool prefix)
    5.55 -      :: map (fn (name, value) =>
    5.56 -                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
    5.57 -                  value |> stringify_raw_param_value
    5.58 -                        |> parse_bool_option false name |> the))
    5.59 -             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
    5.60 +      lookup_assigns read prefix "" (the o parse_bool_option false prefix)
    5.61      fun lookup_bool_option_assigns read prefix =
    5.62 -      (NONE, lookup_bool_option prefix)
    5.63 -      :: map (fn (name, value) =>
    5.64 -                 (SOME (read (String.extract (name, size prefix + 1, NONE))),
    5.65 -                  value |> stringify_raw_param_value
    5.66 -                        |> parse_bool_option true name))
    5.67 -             (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
    5.68 +      lookup_assigns read prefix "" (parse_bool_option true prefix)
    5.69 +    fun lookup_strings_assigns read prefix =
    5.70 +      lookup_assigns read prefix "" (space_explode " ")
    5.71      fun lookup_time name =
    5.72        case lookup name of
    5.73          NONE => NONE
    5.74 @@ -255,6 +251,7 @@
    5.75      val show_datatypes = debug orelse lookup_bool "show_datatypes"
    5.76      val show_consts = debug orelse lookup_bool "show_consts"
    5.77      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
    5.78 +    val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
    5.79      val evals = lookup_term_list "eval"
    5.80      val max_potential =
    5.81        if auto then 0 else Int.max (0, lookup_int "max_potential")
    5.82 @@ -279,9 +276,10 @@
    5.83       peephole_optim = peephole_optim, timeout = timeout,
    5.84       tac_timeout = tac_timeout, max_threads = max_threads,
    5.85       show_datatypes = show_datatypes, show_consts = show_consts,
    5.86 -     formats = formats, evals = evals, max_potential = max_potential,
    5.87 -     max_genuine = max_genuine, check_potential = check_potential,
    5.88 -     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
    5.89 +     formats = formats, atomss = atomss, evals = evals,
    5.90 +     max_potential = max_potential, max_genuine = max_genuine,
    5.91 +     check_potential = check_potential, check_genuine = check_genuine,
    5.92 +     batch_size = batch_size, expect = expect}
    5.93    end
    5.94  
    5.95  fun default_params thy =

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 11:58:50 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 12:20:08 2010 +0200
     6.3 @@ -31,8 +31,9 @@
     6.4      nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
     6.5    val dest_plain_fun : term -> bool * (term list * term list)
     6.6    val reconstruct_hol_model :
     6.7 -    params -> scope -> (term option * int list) list -> styp list -> nut list
     6.8 -    -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
     6.9 +    params -> scope -> (term option * int list) list
    6.10 +    -> (typ option * string list) list -> styp list -> nut list -> nut list
    6.11 +    -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
    6.12      -> Pretty.T * bool
    6.13    val prove_hol_model :
    6.14      scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
    6.15 @@ -103,31 +104,41 @@
    6.16  
    6.17  (** Term reconstruction **)
    6.18  
    6.19 -fun nth_atom_suffix pool s j k =
    6.20 -  (case AList.lookup (op =) (!pool) (s, k) of
    6.21 -     SOME js =>
    6.22 -     (case find_index (curry (op =) j) js of
    6.23 -        ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
    6.24 -               length js + 1)
    6.25 -      | n => length js - n)
    6.26 -   | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
    6.27 -  |> nat_subscript
    6.28 -  |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
    6.29 +fun nth_atom_number pool T j =
    6.30 +  case AList.lookup (op =) (!pool) T of
    6.31 +    SOME js =>
    6.32 +    (case find_index (curry (op =) j) js of
    6.33 +       ~1 => (Unsynchronized.change pool (cons (T, j :: js));
    6.34 +              length js + 1)
    6.35 +     | n => length js - n)
    6.36 +  | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
    6.37 +fun atom_suffix s =
    6.38 +  nat_subscript
    6.39 +  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
    6.40       ? prefix "\<^isub>,"
    6.41 -fun nth_atom_name pool prefix (Type (s, _)) j k =
    6.42 -    let val s' = shortest_name s in
    6.43 -      prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
    6.44 -      nth_atom_suffix pool s j k
    6.45 -    end
    6.46 -  | nth_atom_name pool prefix (TFree (s, _)) j k =
    6.47 -    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
    6.48 -  | nth_atom_name _ _ T _ _ =
    6.49 -    raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
    6.50 -fun nth_atom pool for_auto T j k =
    6.51 +fun nth_atom_name thy atomss pool prefix T j =
    6.52 +  let
    6.53 +    val ss = these (triple_lookup (type_match thy) atomss T)
    6.54 +    val m = nth_atom_number pool T j
    6.55 +  in
    6.56 +    if m <= length ss then
    6.57 +      nth ss (m - 1)
    6.58 +    else case T of
    6.59 +      Type (s, _) =>
    6.60 +      let val s' = shortest_name s in
    6.61 +        prefix ^
    6.62 +        (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
    6.63 +        atom_suffix s m
    6.64 +      end
    6.65 +    | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
    6.66 +    | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
    6.67 +  end
    6.68 +fun nth_atom thy atomss pool for_auto T j =
    6.69    if for_auto then
    6.70 -    Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
    6.71 +    Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
    6.72 +                        T j, T)
    6.73    else
    6.74 -    Const (nth_atom_name pool "" T j k, T)
    6.75 +    Const (nth_atom_name thy atomss pool "" T j, T)
    6.76  
    6.77  fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
    6.78      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
    6.79 @@ -300,14 +311,14 @@
    6.80    strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
    6.81  
    6.82  fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
    6.83 -                       sel_names rel_table bounds card T =
    6.84 +                       atomss sel_names rel_table bounds card T =
    6.85    let
    6.86      val card = if card = 0 then card_of_type card_assigns T else card
    6.87      fun nth_value_of_type n =
    6.88        let
    6.89          fun term unfold =
    6.90 -          reconstruct_term unfold pool wacky_names scope sel_names rel_table
    6.91 -                           bounds T T (Atom (card, 0)) [[n]]
    6.92 +          reconstruct_term unfold pool wacky_names scope atomss sel_names
    6.93 +                           rel_table bounds T T (Atom (card, 0)) [[n]]
    6.94        in
    6.95          case term false of
    6.96            t as Const (s, _) =>
    6.97 @@ -320,7 +331,8 @@
    6.98    in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
    6.99  and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
   6.100          (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
   6.101 -                   bits, datatypes, ofs, ...}) sel_names rel_table bounds =
   6.102 +                   bits, datatypes, ofs, ...})
   6.103 +        atomss sel_names rel_table bounds =
   6.104    let
   6.105      val for_auto = (maybe_name = "")
   6.106      fun value_of_bits jss =
   6.107 @@ -332,7 +344,8 @@
   6.108               js 0
   6.109        end
   6.110      val all_values =
   6.111 -      all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
   6.112 +      all_values_of_type pool wacky_names scope atomss sel_names rel_table
   6.113 +                         bounds 0
   6.114      fun postprocess_term (Type (@{type_name fun}, _)) = I
   6.115        | postprocess_term T =
   6.116          if null (Data.get thy) then
   6.117 @@ -471,16 +484,16 @@
   6.118          else if T = @{typ bisim_iterator} then
   6.119            HOLogic.mk_number nat_T j
   6.120          else case datatype_spec datatypes T of
   6.121 -          NONE => nth_atom pool for_auto T j k
   6.122 -        | SOME {deep = false, ...} => nth_atom pool for_auto T j k
   6.123 +          NONE => nth_atom thy atomss pool for_auto T j
   6.124 +        | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
   6.125          | SOME {co, standard, constrs, ...} =>
   6.126            let
   6.127              fun tuples_for_const (s, T) =
   6.128                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
   6.129              fun cyclic_atom () =
   6.130 -              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
   6.131 -            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
   6.132 -
   6.133 +              nth_atom thy atomss pool for_auto (Type (cyclic_type_name, [])) j
   6.134 +            fun cyclic_var () =
   6.135 +              Var ((nth_atom_name thy atomss pool "" T j, 0), T)
   6.136              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
   6.137                                   constrs
   6.138              val real_j = j + offset_of_type ofs T
   6.139 @@ -612,7 +625,7 @@
   6.140          else term_for_rep true seen T T' R jss
   6.141        | term_for_rep _ _ T _ R jss =
   6.142          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
   6.143 -                   Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
   6.144 +                   Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
   6.145                     string_of_int (length jss))
   6.146    in
   6.147      postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
   6.148 @@ -811,10 +824,10 @@
   6.149  
   6.150  (** Model reconstruction **)
   6.151  
   6.152 -fun term_for_name pool scope sel_names rel_table bounds name =
   6.153 +fun term_for_name pool scope atomss sel_names rel_table bounds name =
   6.154    let val T = type_of name in
   6.155      tuple_list_for_name rel_table bounds name
   6.156 -    |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
   6.157 +    |> reconstruct_term false pool (("", ""), ("", "")) scope atomss sel_names
   6.158                          rel_table bounds T T (rep_of name)
   6.159    end
   6.160  
   6.161 @@ -848,7 +861,8 @@
   6.162                        ground_thm_table, ersatz_table, skolems, special_funs,
   6.163                        unrolled_preds, wf_cache, constr_cache},
   6.164           binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
   6.165 -        formats all_frees free_names sel_names nonsel_names rel_table bounds =
   6.166 +        formats atomss all_frees free_names sel_names nonsel_names rel_table
   6.167 +        bounds =
   6.168    let
   6.169      val pool = Unsynchronized.ref []
   6.170      val (wacky_names as (_, base_step_names), ctxt) =
   6.171 @@ -871,11 +885,10 @@
   6.172        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
   6.173         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
   6.174      fun term_for_rep unfold =
   6.175 -      reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
   6.176 +      reconstruct_term unfold pool wacky_names scope atomss sel_names rel_table
   6.177 +                       bounds
   6.178      fun nth_value_of_type card T n =
   6.179 -      let
   6.180 -        fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
   6.181 -      in
   6.182 +      let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in
   6.183          case aux false of
   6.184            t as Const (s, _) =>
   6.185            if String.isPrefix cyclic_const_prefix s then
   6.186 @@ -885,7 +898,8 @@
   6.187          | t => t
   6.188        end
   6.189      val all_values =
   6.190 -      all_values_of_type pool wacky_names scope sel_names rel_table bounds
   6.191 +      all_values_of_type pool wacky_names scope atomss sel_names rel_table
   6.192 +                         bounds
   6.193      fun is_codatatype_wellformed (cos : dtype_spec list)
   6.194                                   ({typ, card, ...} : dtype_spec) =
   6.195        let
   6.196 @@ -996,9 +1010,10 @@
   6.197                      auto_timeout free_names sel_names rel_table bounds prop =
   6.198    let
   6.199      val pool = Unsynchronized.ref []
   6.200 +    val atomss = [(NONE, [])]
   6.201      fun free_type_assm (T, k) =
   6.202        let
   6.203 -        fun atom j = nth_atom pool true T j k
   6.204 +        fun atom j = nth_atom thy atomss pool true T j
   6.205          fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
   6.206          val eqs = map equation_for_atom (index_seq 0 k)
   6.207          val compreh_assm =
   6.208 @@ -1008,7 +1023,8 @@
   6.209        in s_conj (compreh_assm, distinct_assm) end
   6.210      fun free_name_assm name =
   6.211        HOLogic.mk_eq (Free (nickname_of name, type_of name),
   6.212 -                     term_for_name pool scope sel_names rel_table bounds name)
   6.213 +                     term_for_name pool scope atomss sel_names rel_table bounds
   6.214 +                                   name)
   6.215      val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
   6.216      val model_assms = map free_name_assm free_names
   6.217      val assm = foldr1 s_conj (freeT_assms @ model_assms)

     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jun 01 11:58:50 2010 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jun 01 12:20:08 2010 +0200
     7.3 @@ -290,7 +290,7 @@
     7.4              end
     7.5          else
     7.6            MType (s, [])
     7.7 -      | _ => MType (Refute.string_of_typ T, [])
     7.8 +      | _ => MType (simple_string_of_typ T, [])
     7.9    in do_type end
    7.10  
    7.11  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]

     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 11:58:50 2010 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 12:20:08 2010 +0200
     8.3 @@ -910,14 +910,14 @@
     8.4                                  \add_axioms_for_term",
     8.5                                  "too many nested axioms (" ^
     8.6                                  string_of_int depth ^ ")")
     8.7 -             else if Refute.is_const_of_class thy x then
     8.8 +             else if is_of_class_const thy x then
     8.9                 let
    8.10                   val class = Logic.class_of_const s
    8.11                   val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
    8.12                                                     class)
    8.13                   val ax1 = try (specialize_type thy x) of_class
    8.14                   val ax2 = Option.map (specialize_type thy x o snd)
    8.15 -                                      (Refute.get_classdef thy class)
    8.16 +                                      (get_class_def thy class)
    8.17                 in
    8.18                   fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
    8.19                        accum

     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Jun 01 11:58:50 2010 +0200
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Jun 01 12:20:08 2010 +0200
     9.3 @@ -57,8 +57,15 @@
     9.4    val bool_T : typ
     9.5    val nat_T : typ
     9.6    val int_T : typ
     9.7 +  val simple_string_of_typ : typ -> string
     9.8 +  val is_real_constr : theory -> string * typ -> bool
     9.9 +  val typ_of_dtyp :
    9.10 +    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
    9.11 +    -> typ
    9.12 +  val is_of_class_const : theory -> string * typ -> bool
    9.13 +  val get_class_def : theory -> string -> (string * term) option
    9.14    val monomorphic_term : Type.tyenv -> term -> term
    9.15 -  val specialize_type : theory -> (string * typ) -> term -> term
    9.16 +  val specialize_type : theory -> string * typ -> term -> term
    9.17    val nat_subscript : int -> string
    9.18    val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
    9.19    val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
    9.20 @@ -229,6 +236,11 @@
    9.21  val nat_T = @{typ nat}
    9.22  val int_T = @{typ int}
    9.23  
    9.24 +val simple_string_of_typ = Refute.string_of_typ
    9.25 +val is_real_constr = Refute.is_IDT_constructor
    9.26 +val typ_of_dtyp = Refute.typ_of_dtyp
    9.27 +val is_of_class_const = Refute.is_const_of_class
    9.28 +val get_class_def = Refute.get_classdef
    9.29  val monomorphic_term = Sledgehammer_Util.monomorphic_term
    9.30  val specialize_type = Sledgehammer_Util.specialize_type
    9.31