1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon May 31 18:51:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 01 10:31:18 2010 +0200
     1.3 @@ -439,7 +439,7 @@
     1.4      maps factorize [mk_fst z, mk_snd z]
     1.5    | factorize z = [z]
     1.6  
     1.7 -fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
     1.8 +fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
     1.9    let
    1.10      fun aux eq ss Ts t =
    1.11        let
    1.12 @@ -565,7 +565,7 @@
    1.13            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    1.14          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    1.15            if is_built_in_const thy stds false x then Cst (Suc, T, Any)
    1.16 -          else if is_constr thy stds x then do_construct x []
    1.17 +          else if is_constr ctxt stds x then do_construct x []
    1.18            else ConstName (s, T, Any)
    1.19          | (Const (@{const_name finite}, T), [t1]) =>
    1.20            (if is_finite_type hol_ctxt (domain_type T) then
    1.21 @@ -576,7 +576,7 @@
    1.22          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
    1.23          | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
    1.24            if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
    1.25 -          else if is_constr thy stds x then do_construct x []
    1.26 +          else if is_constr ctxt stds x then do_construct x []
    1.27            else ConstName (s, T, Any)
    1.28          | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
    1.29            if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
    1.30 @@ -653,7 +653,7 @@
    1.31             [t1, t2]) =>
    1.32            Op2 (Union, T1, Any, sub t1, sub t2)
    1.33          | (t0 as Const (x as (s, T)), ts) =>
    1.34 -          if is_constr thy stds x then
    1.35 +          if is_constr ctxt stds x then
    1.36              do_construct x ts
    1.37            else if String.isPrefix numeral_prefix s then
    1.38              Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
    1.39 @@ -687,13 +687,13 @@
    1.40      val R = best_non_opt_set_rep_for_type scope (type_of v)
    1.41      val v = modify_name_rep v R
    1.42    in (v :: vs, NameTable.update (v, R) table) end
    1.43 -fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
    1.44 +fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
    1.45                           (vs, table) =
    1.46    let
    1.47      val x as (s, T) = (nickname_of v, type_of v)
    1.48 -    val R = (if is_abs_fun thy x then
    1.49 +    val R = (if is_abs_fun ctxt x then
    1.50                 rep_for_abs_fun
    1.51 -             else if is_rep_fun thy x then
    1.52 +             else if is_rep_fun ctxt x then
    1.53                 Func oo best_non_opt_symmetric_reps_for_fun_type
    1.54               else if all_exact orelse is_skolem_name v orelse
    1.55                      member (op =) [@{const_name undefined_fast_The},