--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Nov 13 06:24:31 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Nov 13 15:59:53 2009 +0100
@@ -7,6 +7,7 @@
signature NITPICK_MODEL =
sig
+ type styp = Nitpick_Util.styp
type scope = Nitpick_Scope.scope
type rep = Nitpick_Rep.rep
type nut = Nitpick_Nut.nut
@@ -636,7 +637,7 @@
||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
val free_names =
map (fn x as (s, T) =>
- case filter (equal x o nickname_of pairf (unbox_type o type_of))
+ case filter (equal x o pairf nickname_of (unbox_type o type_of))
free_names of
[name] => name
| [] => FreeName (s, T, Any)
@@ -698,8 +699,8 @@
| TimeLimit.TimeOut => false
end
in
- if silence try_out false then SOME true
- else if silence try_out true then SOME false
+ if try_out false then SOME true
+ else if try_out true then SOME false
else NONE
end