--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 10:02:14 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 11:05:32 2010 +0100
@@ -293,15 +293,15 @@
$ do_term new_Ts old_Ts polar t2
| Const (s as @{const_name The}, T) => do_description_operator s T
| Const (s as @{const_name Eps}, T) => do_description_operator s T
- | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
- let val T' = box_type hol_ctxt InFunLHS T in
- Const (@{const_name quot_normal}, T' --> T')
- end
| Const (s as @{const_name Tha}, T) => do_description_operator s T
| Const (x as (s, T)) =>
Const (s, if s = @{const_name converse} orelse
s = @{const_name trancl} then
box_relational_operator_type T
+ else if String.isPrefix quot_normal_prefix s then
+ let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
+ T' --> T'
+ end
else if is_built_in_const thy stds fast_descrs x orelse
s = @{const_name Sigma} then
T
@@ -1022,8 +1022,9 @@
(* hol_context -> term -> (term list * term list) * (bool * bool) *)
fun axioms_for_term
- (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
- evals, def_table, nondef_table, user_nondefs, ...}) t =
+ (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
+ fast_descrs, evals, def_table, nondef_table, user_nondefs,
+ ...}) t =
let
type accumulator = styp list * (term list * term list)
(* (term list * term list -> term list)
@@ -1134,7 +1135,8 @@
#> (if is_pure_typedef thy T then
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
else if is_quot_type thy T then
- fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
+ fold (add_def_axiom depth)
+ (optimized_quot_type_axioms ctxt stds z)
else if max_bisim_depth >= 0 andalso is_codatatype thy T then
fold (add_maybe_def_axiom depth)
(codatatype_bisim_axioms hol_ctxt T)