src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 35311 8f9a66fc9f80
parent 35284 9edc2bd6d2bd
child 35312 99cd1f96b400
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 10:02:14 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 11:05:32 2010 +0100
     1.3 @@ -293,15 +293,15 @@
     1.4          $ do_term new_Ts old_Ts polar t2
     1.5        | Const (s as @{const_name The}, T) => do_description_operator s T
     1.6        | Const (s as @{const_name Eps}, T) => do_description_operator s T
     1.7 -      | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
     1.8 -        let val T' = box_type hol_ctxt InFunLHS T in
     1.9 -          Const (@{const_name quot_normal}, T' --> T')
    1.10 -        end
    1.11        | Const (s as @{const_name Tha}, T) => do_description_operator s T
    1.12        | Const (x as (s, T)) =>
    1.13          Const (s, if s = @{const_name converse} orelse
    1.14                       s = @{const_name trancl} then
    1.15                      box_relational_operator_type T
    1.16 +                  else if String.isPrefix quot_normal_prefix s then
    1.17 +                    let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
    1.18 +                      T' --> T'
    1.19 +                    end
    1.20                    else if is_built_in_const thy stds fast_descrs x orelse
    1.21                            s = @{const_name Sigma} then
    1.22                      T
    1.23 @@ -1022,8 +1022,9 @@
    1.24  
    1.25  (* hol_context -> term -> (term list * term list) * (bool * bool) *)
    1.26  fun axioms_for_term
    1.27 -        (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
    1.28 -                      evals, def_table, nondef_table, user_nondefs, ...}) t =
    1.29 +        (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
    1.30 +                      fast_descrs, evals, def_table, nondef_table, user_nondefs,
    1.31 +                      ...}) t =
    1.32    let
    1.33      type accumulator = styp list * (term list * term list)
    1.34      (* (term list * term list -> term list)
    1.35 @@ -1134,7 +1135,8 @@
    1.36          #> (if is_pure_typedef thy T then
    1.37                fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
    1.38              else if is_quot_type thy T then
    1.39 -              fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
    1.40 +              fold (add_def_axiom depth)
    1.41 +                   (optimized_quot_type_axioms ctxt stds z)
    1.42              else if max_bisim_depth >= 0 andalso is_codatatype thy T then
    1.43                fold (add_maybe_def_axiom depth)
    1.44                     (codatatype_bisim_axioms hol_ctxt T)