--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Aug 03 21:20:31 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Aug 03 21:37:12 2010 +0200
@@ -1106,8 +1106,9 @@
fun solve_any_problem overlord deadline max_threads max_solutions problems =
let
- fun do_solve () = uncached_solve_any_problem overlord deadline max_threads
- max_solutions problems
+ fun do_solve () =
+ uncached_solve_any_problem overlord deadline max_threads max_solutions
+ problems
in
if overlord then
do_solve ()
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Aug 03 21:20:31 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Aug 03 21:37:12 2010 +0200
@@ -937,7 +937,7 @@
end
fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
Pretty.block (Pretty.breaks
- (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
+ (pretty_for_type ctxt typ ::
(case typ of
Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
| Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]