tuning
authorblanchet
Tue Aug 03 21:37:12 2010 +0200 (2010-08-03)
changeset 38189a493dc2179a3
parent 38188 7f12a03c513c
child 38190 b02e204b613a
tuning
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Aug 03 21:20:31 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Aug 03 21:37:12 2010 +0200
     1.3 @@ -1106,8 +1106,9 @@
     1.4  
     1.5  fun solve_any_problem overlord deadline max_threads max_solutions problems =
     1.6    let
     1.7 -    fun do_solve () = uncached_solve_any_problem overlord deadline max_threads
     1.8 -                                                 max_solutions problems
     1.9 +    fun do_solve () =
    1.10 +      uncached_solve_any_problem overlord deadline max_threads max_solutions
    1.11 +                                 problems
    1.12    in
    1.13      if overlord then
    1.14        do_solve ()
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Aug 03 21:20:31 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Aug 03 21:37:12 2010 +0200
     2.3 @@ -937,7 +937,7 @@
     2.4        end
     2.5      fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
     2.6        Pretty.block (Pretty.breaks
     2.7 -          (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
     2.8 +          (pretty_for_type ctxt typ ::
     2.9             (case typ of
    2.10                Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
    2.11              | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]