# HG changeset patch
# User blanchet
# Date 1275381078 -7200
# Node ID 0dca1ec52999283d101c632362ddc14b7e7eecb4
# Parent  da728f9a68e837feb2b680846bf59a15db97fb8d
thread along context instead of theory for typedef lookup

diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -242,7 +242,7 @@
 *)
     val max_bisim_depth = fold Integer.max bisim_depths ~1
     val case_names = case_const_names thy stds
-    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
+    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
     val def_table = const_def_table ctxt subst defs
     val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
     val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
@@ -322,8 +322,8 @@
         ". " ^ extra
       end
     fun is_type_fundamentally_monotonic T =
-      (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
-       (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
+      (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso
+       (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
       is_number_type thy T orelse is_bit_type T
     fun is_type_actually_monotonic T =
       formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
@@ -369,7 +369,8 @@
       else
         ()
     val (deep_dataTs, shallow_dataTs) =
-      all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
+      all_Ts |> filter (is_datatype ctxt stds)
+             |> List.partition is_datatype_deep
     val finitizable_dataTs =
       shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
                      |> filter is_shallow_datatype_finitizable
diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -109,20 +109,19 @@
   val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
   val is_quot_type : theory -> typ -> bool
   val is_codatatype : theory -> typ -> bool
-  val is_pure_typedef : theory -> typ -> bool
-  val is_univ_typedef : theory -> typ -> bool
-  val is_datatype : theory -> (typ option * bool) list -> typ -> bool
+  val is_pure_typedef : Proof.context -> typ -> bool
+  val is_univ_typedef : Proof.context -> typ -> bool
+  val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
   val is_record_constr : styp -> bool
   val is_record_get : theory -> styp -> bool
   val is_record_update : theory -> styp -> bool
-  val is_abs_fun : theory -> styp -> bool
-  val is_rep_fun : theory -> styp -> bool
+  val is_abs_fun : Proof.context -> styp -> bool
+  val is_rep_fun : Proof.context -> styp -> bool
   val is_quot_abs_fun : Proof.context -> styp -> bool
   val is_quot_rep_fun : Proof.context -> styp -> bool
-  val mate_of_rep_fun : theory -> styp -> styp
-  val is_constr_like : theory -> styp -> bool
-  val is_stale_constr : theory -> styp -> bool
-  val is_constr : theory -> (typ option * bool) list -> styp -> bool
+  val mate_of_rep_fun : Proof.context -> styp -> styp
+  val is_constr_like : Proof.context -> styp -> bool
+  val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
   val is_sel : string -> bool
   val is_sel_like_and_no_discr : string -> bool
   val box_type : hol_context -> boxability -> typ -> typ
@@ -151,9 +150,10 @@
   val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
   val discriminate_value : hol_context -> styp -> term -> term
   val select_nth_constr_arg :
-    theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
+    Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
+    -> term
   val construct_value :
-    theory -> (typ option * bool) list -> styp -> term list -> term
+    Proof.context -> (typ option * bool) list -> styp -> term list -> term
   val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
   val card_of_type : (typ * int) list -> typ -> int
   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
@@ -165,7 +165,7 @@
   val abs_var : indexname * typ -> term -> term
   val is_funky_typedef : theory -> typ -> bool
   val all_axioms_of :
-    theory -> (term * term) list -> term list * term list * term list
+    Proof.context -> (term * term) list -> term list * term list * term list
   val arity_of_built_in_const :
     theory -> (typ option * bool) list -> bool -> styp -> int option
   val is_built_in_const :
@@ -186,8 +186,8 @@
   val ground_theorem_table : theory -> term list Inttab.table
   val ersatz_table : theory -> (string * string) list
   val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
-  val inverse_axioms_for_rep_fun : theory -> styp -> term list
-  val optimized_typedef_axioms : theory -> string * typ list -> term list
+  val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
+  val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
   val optimized_quot_type_axioms :
     Proof.context -> (typ option * bool) list -> string * typ list -> term list
   val def_of_const : theory -> const_table -> styp -> term option
@@ -196,8 +196,8 @@
     theory -> const_table -> string * typ -> fixpoint_kind
   val is_inductive_pred : hol_context -> styp -> bool
   val is_equational_fun : hol_context -> styp -> bool
-  val is_constr_pattern_lhs : theory -> term -> bool
-  val is_constr_pattern_formula : theory -> term -> bool
+  val is_constr_pattern_lhs : Proof.context -> term -> bool
+  val is_constr_pattern_formula : Proof.context -> term -> bool
   val nondef_props_for_const :
     theory -> bool -> const_table -> styp -> term list
   val is_choice_spec_fun : hol_context -> styp -> bool
@@ -524,22 +524,24 @@
    set_def: thm option, prop_of_Rep: thm, set_name: string,
    Abs_inverse: thm option, Rep_inverse: thm option}
 
-fun typedef_info thy s =
-  if is_frac_type thy (Type (s, [])) then
-    SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
-          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
-          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
-                          |> Logic.varify_global,
-          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
-  else case Typedef.get_info_global thy s of
-    (* FIXME handle multiple typedef interpretations (!??) *)
-    [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
-          Rep_inverse, ...})] =>
-    SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
-          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
-          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
-          Rep_inverse = SOME Rep_inverse}
-  | _ => NONE
+fun typedef_info ctxt s =
+  let val thy = ProofContext.theory_of ctxt in
+    if is_frac_type thy (Type (s, [])) then
+      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
+            Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
+            set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
+                            |> Logic.varify_global,
+            set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
+    else case Typedef.get_info ctxt s of
+      (* ### multiple *)
+      [({abs_type, rep_type, Abs_name, Rep_name, ...},
+        {set_def, Rep, Abs_inverse, Rep_inverse, ...})] =>
+      SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
+            Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
+            set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+            Rep_inverse = SOME Rep_inverse}
+    | _ => NONE
+  end
 
 val is_typedef = is_some oo typedef_info
 val is_real_datatype = is_some oo Datatype.get_info
@@ -594,14 +596,16 @@
     not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
                |> Option.map snd |> these))
   | is_codatatype _ _ = false
-fun is_pure_typedef thy (T as Type (s, _)) =
-    is_typedef thy s andalso
-    not (is_real_datatype thy s orelse is_quot_type thy T orelse
-         is_codatatype thy T orelse is_record_type T orelse
-         is_integer_like_type T)
+fun is_pure_typedef ctxt (T as Type (s, _)) =
+    let val thy = ProofContext.theory_of ctxt in
+      is_typedef ctxt s andalso
+      not (is_real_datatype thy s orelse is_quot_type thy T orelse
+           is_codatatype thy T orelse is_record_type T orelse
+           is_integer_like_type T)
+    end
   | is_pure_typedef _ _ = false
-fun is_univ_typedef thy (Type (s, _)) =
-    (case typedef_info thy s of
+fun is_univ_typedef ctxt (Type (s, _)) =
+    (case typedef_info ctxt s of
        SOME {set_def, prop_of_Rep, ...} =>
        let
          val t_opt =
@@ -623,9 +627,11 @@
        end
      | NONE => false)
   | is_univ_typedef _ _ = false
-fun is_datatype thy stds (T as Type (s, _)) =
-    (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
-     is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+fun is_datatype ctxt stds (T as Type (s, _)) =
+    let val thy = ProofContext.theory_of ctxt in
+      (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
+       is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+    end
   | is_datatype _ _ _ = false
 
 fun all_record_fields thy T =
@@ -651,13 +657,13 @@
   exists (curry (op =) (unsuffix Record.updateN s) o fst)
          (all_record_fields thy (body_type T))
   handle TYPE _ => false
-fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
-    (case typedef_info thy s' of
+fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
+    (case typedef_info ctxt s' of
        SOME {Abs_name, ...} => s = Abs_name
      | NONE => false)
   | is_abs_fun _ _ = false
-fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
-    (case typedef_info thy s' of
+fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
+    (case typedef_info ctxt s' of
        SOME {Rep_name, ...} => s = Rep_name
      | NONE => false)
   | is_rep_fun _ _ = false
@@ -672,9 +678,9 @@
      = SOME (Const x))
   | is_quot_rep_fun _ _ = false
 
-fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
-                                        [T1 as Type (s', _), T2]))) =
-    (case typedef_info thy s' of
+fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
+                                         [T1 as Type (s', _), T2]))) =
+    (case typedef_info ctxt s' of
        SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
@@ -700,23 +706,30 @@
            (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
   end
   handle TYPE ("dest_Type", _, _) => false
-fun is_constr_like thy (s, T) =
+fun is_constr_like ctxt (s, T) =
   member (op =) [@{const_name FinFun}, @{const_name FunBox},
                  @{const_name PairBox}, @{const_name Quot},
                  @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
-  let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
+  let
+    val thy = ProofContext.theory_of ctxt
+    val (x as (_, T)) = (s, unarize_unbox_etc_type T)
+  in
     Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
-    (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
+    (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
     is_coconstr thy x
   end
-fun is_stale_constr thy (x as (_, T)) =
-  is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
-  not (is_coconstr thy x)
-fun is_constr thy stds (x as (_, T)) =
-  is_constr_like thy x andalso
-  not (is_basic_datatype thy stds
+fun is_stale_constr ctxt (x as (_, T)) =
+  let val thy = ProofContext.theory_of ctxt in
+    is_codatatype thy (body_type T) andalso is_constr_like ctxt x andalso
+    not (is_coconstr thy x)
+  end
+fun is_constr ctxt stds (x as (_, T)) =
+  let val thy = ProofContext.theory_of ctxt in
+    is_constr_like ctxt x andalso
+    not (is_basic_datatype thy stds
                          (fst (dest_Type (unarize_type (body_type T))))) andalso
-  not (is_stale_constr thy x)
+    not (is_stale_constr ctxt x)
+  end
 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
 val is_sel_like_and_no_discr =
   String.isPrefix sel_prefix orf
@@ -836,12 +849,12 @@
 fun zero_const T = Const (@{const_name zero_class.zero}, T)
 fun suc_const T = Const (@{const_name Suc}, T --> T)
 
-fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
+fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
                               (T as Type (s, Ts)) =
     (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
        SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
      | _ =>
-       if is_datatype thy stds T then
+       if is_datatype ctxt stds T then
          case Datatype.get_info thy s of
            SOME {index, descr, ...} =>
            let
@@ -860,7 +873,7 @@
              in [(s', T')] end
            else if is_quot_type thy T then
              [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
-           else case typedef_info thy s of
+           else case typedef_info ctxt s of
              SOME {abs_type, rep_type, Abs_name, ...} =>
              [(Abs_name,
                varify_and_instantiate_type thy abs_type T rep_type --> T)]
@@ -905,11 +918,11 @@
     else
       Abs (Name.uu, dataT, @{const True})
   end
-fun discriminate_value (hol_ctxt as {thy, ...}) x t =
+fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
   case head_of t of
     Const x' =>
     if x = x' then @{const True}
-    else if is_constr_like thy x' then @{const False}
+    else if is_constr_like ctxt x' then @{const False}
     else betapply (discr_term_for_constr hol_ctxt x, t)
   | _ => betapply (discr_term_for_constr hol_ctxt x, t)
 
@@ -933,24 +946,26 @@
                      (List.take (arg_Ts, n)) 0
       in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   end
-fun select_nth_constr_arg thy stds x t n res_T =
-  (case strip_comb t of
-     (Const x', args) =>
-     if x = x' then nth args n
-     else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
-     else raise SAME ()
-   | _ => raise SAME())
-  handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+fun select_nth_constr_arg ctxt stds x t n res_T =
+  let val thy = ProofContext.theory_of ctxt in
+    (case strip_comb t of
+       (Const x', args) =>
+       if x = x' then nth args n
+       else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
+       else raise SAME ()
+     | _ => raise SAME())
+    handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+  end
 
 fun construct_value _ _ x [] = Const x
-  | construct_value thy stds (x as (s, _)) args =
+  | construct_value ctxt stds (x as (s, _)) args =
     let val args = map Envir.eta_contract args in
       case hd args of
         Const (s', _) $ t =>
         if is_sel_like_and_no_discr s' andalso
            constr_name_for_sel_like s' = s andalso
            forall (fn (n, t') =>
-                      select_nth_constr_arg thy stds x t n dummyT = t')
+                      select_nth_constr_arg ctxt stds x t n dummyT = t')
                   (index_seq 0 (length args) ~~ args) then
           t
         else
@@ -958,9 +973,9 @@
       | _ => list_comb (Const x, args)
     end
 
-fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
+fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
   (case head_of t of
-     Const x => if is_constr_like thy x then t else raise SAME ()
+     Const x => if is_constr_like ctxt x then t else raise SAME ()
    | _ => raise SAME ())
   handle SAME () =>
          let
@@ -973,7 +988,7 @@
                datatype_constrs hol_ctxt T |> hd
            val arg_Ts = binder_types T'
          in
-           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
+           list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
                                      (index_seq 0 (length arg_Ts)) arg_Ts)
          end
 
@@ -985,7 +1000,7 @@
   | _ => t
 fun coerce_bound_0_in_term hol_ctxt new_T old_T =
   old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+and coerce_term (hol_ctxt as {ctxt, stds, fast_descrs, ...}) Ts new_T old_T t =
   if old_T = new_T then
     t
   else
@@ -999,7 +1014,7 @@
                  |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
          |> Envir.eta_contract
          |> new_s <> @{type_name fun}
-            ? construct_value thy stds
+            ? construct_value ctxt stds
                   (if new_s = @{type_name fin_fun} then @{const_name FinFun}
                    else @{const_name FunBox},
                    Type (@{type_name fun}, new_Ts) --> new_T)
@@ -1014,12 +1029,12 @@
           if new_s = @{type_name fun} then
             coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
           else
-            construct_value thy stds
+            construct_value ctxt stds
                 (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
                 [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
                              (Type (@{type_name fun}, old_Ts)) t1]
         | Const _ $ t1 $ t2 =>
-          construct_value thy stds
+          construct_value ctxt stds
               (if new_s = @{type_name "*"} then @{const_name Pair}
                else @{const_name PairBox}, new_Ts ---> new_T)
               (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
@@ -1145,13 +1160,15 @@
 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
                          $ Const (@{const_name TYPE}, _)) = true
   | is_arity_type_axiom _ = false
-fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
-    is_typedef_axiom thy boring t2
-  | is_typedef_axiom thy boring
+fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
+    is_typedef_axiom ctxt boring t2
+  | is_typedef_axiom ctxt boring
         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
          $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
          $ Const _ $ _)) =
-    boring <> is_funky_typedef_name thy s andalso is_typedef thy s
+    let val thy = ProofContext.theory_of ctxt in
+      boring <> is_funky_typedef_name thy s andalso is_typedef ctxt s
+    end
   | is_typedef_axiom _ _ _ = false
 val is_class_axiom =
   Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
@@ -1160,13 +1177,13 @@
    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
    Typedef axioms are uninteresting to Nitpick, because it can retrieve them
    using "typedef_info". *)
-fun partition_axioms_by_definitionality thy axioms def_names =
+fun partition_axioms_by_definitionality ctxt axioms def_names =
   let
     val axioms = sort (fast_string_ord o pairself fst) axioms
     val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
     val nondefs =
       OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
-      |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
+      |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
   in pairself (map snd) (defs, nondefs) end
 
 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
@@ -1189,8 +1206,9 @@
       | do_eq _ = false
   in do_eq end
 
-fun all_axioms_of thy subst =
+fun all_axioms_of ctxt subst =
   let
+    val thy = ProofContext.theory_of ctxt
     val axioms_of_thys =
       maps Thm.axioms_of
       #> map (apsnd (subst_atomic subst o prop_of))
@@ -1203,12 +1221,12 @@
     val built_in_axioms = axioms_of_thys built_in_thys
     val user_axioms = axioms_of_thys user_thys
     val (built_in_defs, built_in_nondefs) =
-      partition_axioms_by_definitionality thy built_in_axioms def_names
-      ||> filter (is_typedef_axiom thy false)
+      partition_axioms_by_definitionality ctxt built_in_axioms def_names
+      ||> filter (is_typedef_axiom ctxt false)
     val (user_defs, user_nondefs) =
-      partition_axioms_by_definitionality thy user_axioms def_names
+      partition_axioms_by_definitionality ctxt user_axioms def_names
     val (built_in_nondefs, user_nondefs) =
-      List.partition (is_typedef_axiom thy false) user_nondefs
+      List.partition (is_typedef_axiom ctxt false) user_nondefs
       |>> append built_in_nondefs
     val defs =
       (thy |> PureThy.all_thms_of
@@ -1369,16 +1387,16 @@
   | _ => NONE
 fun is_constr_pattern _ (Bound _) = true
   | is_constr_pattern _ (Var _) = true
-  | is_constr_pattern thy t =
+  | is_constr_pattern ctxt t =
     case strip_comb t of
       (Const x, args) =>
-      is_constr_like thy x andalso forall (is_constr_pattern thy) args
+      is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
     | _ => false
-fun is_constr_pattern_lhs thy t =
-  forall (is_constr_pattern thy) (snd (strip_comb t))
-fun is_constr_pattern_formula thy t =
+fun is_constr_pattern_lhs ctxt t =
+  forall (is_constr_pattern ctxt) (snd (strip_comb t))
+fun is_constr_pattern_formula ctxt t =
   case lhs_of_equation t of
-    SOME t' => is_constr_pattern_lhs thy t'
+    SOME t' => is_constr_pattern_lhs ctxt t'
   | NONE => false
 
 (* Similar to "specialize_type" but returns all matches rather than only the
@@ -1439,26 +1457,26 @@
 
 (** Constant unfolding **)
 
-fun constr_case_body thy stds (j, (x as (_, T))) =
+fun constr_case_body ctxt stds (j, (x as (_, T))) =
   let val arg_Ts = binder_types T in
-    list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
+    list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
                              (index_seq 0 (length arg_Ts)) arg_Ts)
   end
-fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
+fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
   Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
-  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
+  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
   $ res_t
-fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
+fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
   let
     val xs = datatype_constrs hol_ctxt dataT
     val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
     val (xs', x) = split_last xs
   in
-    constr_case_body thy stds (1, x)
+    constr_case_body ctxt stds (1, x)
     |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   end
-fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
+fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
   let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
     case no_of_record_field thy s rec_T of
       ~1 => (case rec_T of
@@ -1467,14 +1485,15 @@
                  val rec_T' = List.last Ts
                  val j = num_record_fields thy rec_T - 1
                in
-                 select_nth_constr_arg thy stds constr_x t j res_T
+                 select_nth_constr_arg ctxt stds constr_x t j res_T
                  |> optimized_record_get hol_ctxt s rec_T' res_T
                end
              | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
                                 []))
-    | j => select_nth_constr_arg thy stds constr_x t j res_T
+    | j => select_nth_constr_arg ctxt stds constr_x t j res_T
   end
-fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
+fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
+                            rec_t =
   let
     val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
     val Ts = binder_types constr_T
@@ -1482,7 +1501,7 @@
     val special_j = no_of_record_field thy s rec_T
     val ts =
       map2 (fn j => fn T =>
-               let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
+               let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
                  if j = special_j then
                    betapply (fun_t, t)
                  else if j = n - 1 andalso special_j = ~1 then
@@ -1551,9 +1570,9 @@
       | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
     and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
         (Abs (Name.uu, body_type T,
-              select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
+              select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
       | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
-        (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
+        (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
     and do_const depth Ts t (x as (s, T)) ts =
       case AList.lookup (op =) ersatz_table s of
         SOME s' =>
@@ -1573,9 +1592,9 @@
                  |> do_term (depth + 1) Ts, ts)
               end
             | _ =>
-              if is_constr thy stds x then
+              if is_constr ctxt stds x then
                 (Const x, ts)
-              else if is_stale_constr thy x then
+              else if is_stale_constr ctxt x then
                 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
                                      \(\"" ^ s ^ "\")")
               else if is_quot_abs_fun ctxt x then
@@ -1606,9 +1625,9 @@
                             (do_term depth Ts (hd ts))
                             (do_term depth Ts (nth ts 1)), [])
                 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
-              else if is_rep_fun thy x then
-                let val x' = mate_of_rep_fun thy x in
-                  if is_constr thy stds x' then
+              else if is_rep_fun ctxt x then
+                let val x' = mate_of_rep_fun ctxt x in
+                  if is_constr ctxt stds x' then
                     select_nth_constr_arg_with_args depth Ts x' ts 0
                                                     (range_type T)
                   else
@@ -1679,18 +1698,24 @@
   Unsynchronized.change simp_table
       (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
 
-fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
-  let val abs_T = domain_type T in
-    typedef_info thy (fst (dest_Type abs_T)) |> the
+fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val abs_T = domain_type T
+  in
+    typedef_info ctxt (fst (dest_Type abs_T)) |> the
     |> pairf #Abs_inverse #Rep_inverse
     |> pairself (specialize_type thy x o prop_of o the)
     ||> single |> op ::
   end
-fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
-  let val abs_T = Type abs_z in
-    if is_univ_typedef thy abs_T then
+fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val abs_T = Type abs_z
+  in
+    if is_univ_typedef ctxt abs_T then
       []
-    else case typedef_info thy abs_s of
+    else case typedef_info ctxt abs_s of
       SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
       let
         val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
@@ -1718,7 +1743,7 @@
     val x_var = Var (("x", 0), rep_T)
     val y_var = Var (("y", 0), rep_T)
     val x = (@{const_name Quot}, rep_T --> abs_T)
-    val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
+    val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
     val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
     val normal_x = normal_t $ x_var
     val normal_y = normal_t $ y_var
@@ -1736,7 +1761,7 @@
           HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
   end
 
-fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {ctxt, thy, stds, ...}) T =
   let
     val xs = datatype_constrs hol_ctxt T
     val set_T = T --> bool_T
@@ -1753,8 +1778,8 @@
     fun nth_sub_bisim x n nth_T =
       (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
        else HOLogic.eq_const nth_T)
-      $ select_nth_constr_arg thy stds x x_var n nth_T
-      $ select_nth_constr_arg thy stds x y_var n nth_T
+      $ select_nth_constr_arg ctxt stds x x_var n nth_T
+      $ select_nth_constr_arg ctxt stds x y_var n nth_T
     fun case_func (x as (_, T)) =
       let
         val arg_Ts = binder_types T
diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -319,7 +319,7 @@
       end
   in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
 and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
-        (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
+        (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
                    bits, datatypes, ofs, ...}) sel_names rel_table bounds =
   let
     val for_auto = (maybe_name = "")
@@ -536,7 +536,7 @@
                     | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
                                        \term_for_atom (Abs_Frac)", ts)
                   else if not for_auto andalso
-                          (is_abs_fun thy constr_x orelse
+                          (is_abs_fun ctxt constr_x orelse
                            constr_s = @{const_name Quot}) then
                     Const (abs_name, constr_T) $ the_single ts
                   else
diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -162,8 +162,8 @@
   | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
     could_exist_alpha_subtype alpha_T T
-  | could_exist_alpha_sub_mtype thy alpha_T T =
-    (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
+  | could_exist_alpha_sub_mtype ctxt alpha_T T =
+    (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)
 
 fun exists_alpha_sub_mtype MAlpha = true
   | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
@@ -243,7 +243,7 @@
             else
               S Minus
   in (M1, a, M2) end
-and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
+and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
                                     datatype_mcache, constr_mcache, ...})
                          all_minus =
   let
@@ -255,7 +255,7 @@
         MFun (fresh_mfun_for_fun_type mdata false T1 T2)
       | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
       | Type (z as (s, _)) =>
-        if could_exist_alpha_sub_mtype thy alpha_T T then
+        if could_exist_alpha_sub_mtype ctxt alpha_T T then
           case AList.lookup (op =) (!datatype_mcache) z of
             SOME M => M
           | NONE =>
@@ -304,9 +304,9 @@
           case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
   end
 
-fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
+fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache,
                                 ...}) (x as (_, T)) =
-  if could_exist_alpha_sub_mtype thy alpha_T T then
+  if could_exist_alpha_sub_mtype ctxt alpha_T T then
     case AList.lookup (op =) (!constr_mcache) x of
       SOME M => M
     | NONE => if T = alpha_T then
@@ -741,7 +741,7 @@
                   do_robust_set_operation T accum
                 else if is_sel s then
                   (mtype_for_sel mdata x, accum)
-                else if is_constr thy stds x then
+                else if is_constr ctxt stds x then
                   (mtype_for_constr mdata x, accum)
                 else if is_built_in_const thy stds fast_descrs x then
                   (fresh_mtype_for_type mdata true T, accum)
@@ -924,8 +924,8 @@
   if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
   else consider_general_formula mdata Plus t
 
-fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
-  if not (is_constr_pattern_formula thy t) then
+fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
+  if not (is_constr_pattern_formula ctxt t) then
     consider_nondefinitional_axiom mdata t
   else if is_harmless_axiom mdata t then
     pair (MRaw (t, dummy_M))
@@ -1027,7 +1027,8 @@
 fun fin_fun_constr T1 T2 =
   (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
 
-fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
+fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache,
+                                ...})
                   binarize finitizes alpha_T tsp =
   case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
     SOME (lits, msp, constr_mtypes) =>
@@ -1085,7 +1086,7 @@
                   Const (s, T')
                 else if is_built_in_const thy stds fast_descrs x then
                   coerce_term hol_ctxt Ts T' T t
-                else if is_constr thy stds x then
+                else if is_constr ctxt stds x then
                   Const (finitize_constr x)
                 else if is_sel s then
                   let
@@ -1112,7 +1113,7 @@
                 case T1 of
                   Type (s, [T11, T12]) => 
                   (if s = @{type_name fin_fun} then
-                     select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
+                     select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
                                            0 (T11 --> T12)
                    else
                      t1, T11)
@@ -1127,7 +1128,7 @@
             in
               Abs (s, T, t')
               |> should_finitize (T --> T') a
-                 ? construct_value thy stds (fin_fun_constr T T') o single
+                 ? construct_value ctxt stds (fin_fun_constr T T') o single
             end
       in
         Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -439,7 +439,7 @@
     maps factorize [mk_fst z, mk_snd z]
   | factorize z = [z]
 
-fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
   let
     fun aux eq ss Ts t =
       let
@@ -565,7 +565,7 @@
           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (x as (s as @{const_name Suc}, T)), []) =>
           if is_built_in_const thy stds false x then Cst (Suc, T, Any)
-          else if is_constr thy stds x then do_construct x []
+          else if is_constr ctxt stds x then do_construct x []
           else ConstName (s, T, Any)
         | (Const (@{const_name finite}, T), [t1]) =>
           (if is_finite_type hol_ctxt (domain_type T) then
@@ -576,7 +576,7 @@
         | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
         | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
           if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
-          else if is_constr thy stds x then do_construct x []
+          else if is_constr ctxt stds x then do_construct x []
           else ConstName (s, T, Any)
         | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
           if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
@@ -653,7 +653,7 @@
            [t1, t2]) =>
           Op2 (Union, T1, Any, sub t1, sub t2)
         | (t0 as Const (x as (s, T)), ts) =>
-          if is_constr thy stds x then
+          if is_constr ctxt stds x then
             do_construct x ts
           else if String.isPrefix numeral_prefix s then
             Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
@@ -687,13 +687,13 @@
     val R = best_non_opt_set_rep_for_type scope (type_of v)
     val v = modify_name_rep v R
   in (v :: vs, NameTable.update (v, R) table) end
-fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
+fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
                          (vs, table) =
   let
     val x as (s, T) = (nickname_of v, type_of v)
-    val R = (if is_abs_fun thy x then
+    val R = (if is_abs_fun ctxt x then
                rep_for_abs_fun
-             else if is_rep_fun thy x then
+             else if is_rep_fun ctxt x then
                Func oo best_non_opt_symmetric_reps_for_fun_type
              else if all_exact orelse is_skolem_name v orelse
                     member (op =) [@{const_name undefined_fast_The},
diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -65,14 +65,15 @@
 
 (** Uncurrying **)
 
-fun add_to_uncurry_table thy t =
+fun add_to_uncurry_table ctxt t =
   let
+    val thy = ProofContext.theory_of ctxt
     fun aux (t1 $ t2) args table =
         let val table = aux t2 [] table in aux t1 (t2 :: args) table end
       | aux (Abs (_, _, t')) _ table = aux t' [] table
       | aux (t as Const (x as (s, _))) args table =
         if is_built_in_const thy [(NONE, true)] true x orelse
-           is_constr_like thy x orelse
+           is_constr_like ctxt x orelse
            is_sel s orelse s = @{const_name Sigma} then
           table
         else
@@ -121,8 +122,8 @@
 
 (** Boxing **)
 
-fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
-                             orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})
+                             def orig_t =
   let
     fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
         Type (@{type_name fun}, map box_relational_operator_type Ts)
@@ -228,10 +229,9 @@
                   else if is_built_in_const thy stds fast_descrs x orelse
                           s = @{const_name Sigma} then
                     T
-                  else if is_constr_like thy x then
+                  else if is_constr_like ctxt x then
                     box_type hol_ctxt InConstr T
-                  else if is_sel s
-                       orelse is_rep_fun thy x then
+                  else if is_sel s orelse is_rep_fun ctxt x then
                     box_type hol_ctxt InSel T
                   else
                     box_type hol_ctxt InExpr T)
@@ -248,7 +248,7 @@
           betapply (if s1 = @{type_name fun} then
                       t1
                     else
-                      select_nth_constr_arg thy stds
+                      select_nth_constr_arg ctxt stds
                           (@{const_name FunBox},
                            Type (@{type_name fun}, Ts1) --> T1) t1 0
                           (Type (@{type_name fun}, Ts1)), t2)
@@ -265,7 +265,7 @@
           betapply (if s1 = @{type_name fun} then
                       t1
                     else
-                      select_nth_constr_arg thy stds
+                      select_nth_constr_arg ctxt stds
                           (@{const_name FunBox},
                            Type (@{type_name fun}, Ts1) --> T1) t1 0
                           (Type (@{type_name fun}, Ts1)), t2)
@@ -293,12 +293,12 @@
       | aux _ = true
   in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
 
-fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
+fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t
                          args seen =
   let val t_comb = list_comb (t, args) in
     case t of
       Const x =>
-      if not relax andalso is_constr thy stds x andalso
+      if not relax andalso is_constr ctxt stds x andalso
          not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
          has_heavy_bounds_or_vars Ts t_comb andalso
          not (loose_bvar (t_comb, level)) then
@@ -397,7 +397,7 @@
       $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
     end
 
-fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
+fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
   let
     val num_occs_of_var =
       fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
@@ -432,7 +432,7 @@
             val n = length arg_Ts
           in
             if length args = n andalso
-               (is_constr thy stds x orelse s = @{const_name Pair} orelse
+               (is_constr ctxt stds x orelse s = @{const_name Pair} orelse
                 x = (@{const_name Suc}, nat_T --> nat_T)) andalso
                (not careful orelse not (is_Var t1) orelse
                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
@@ -449,7 +449,7 @@
                         else t0 $ aux false t2 $ aux false t1
     and sel_eq x t n nth_T nth_t =
       HOLogic.eq_const nth_T $ nth_t
-                             $ select_nth_constr_arg thy stds x t n nth_T
+                             $ select_nth_constr_arg ctxt stds x t n nth_T
       |> aux false
   in aux axiom t end
 
@@ -484,7 +484,7 @@
         aux (t1 :: prems) (Term.add_vars t1 zs) t2
   in aux [] [] end
 
-fun find_bound_assign thy stds j =
+fun find_bound_assign ctxt stds j =
   let
     fun do_term _ [] = NONE
       | do_term seen (t :: ts) =
@@ -497,8 +497,9 @@
              | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
                if j' = j andalso
                   s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
-                 SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
-                                       [t2], ts @ seen)
+                 SOME (construct_value ctxt stds
+                                       (@{const_name FunBox}, T2 --> T1) [t2],
+                       ts @ seen)
                else
                  raise SAME ()
              | _ => raise SAME ())
@@ -523,11 +524,11 @@
       | aux _ = raise SAME ()
   in aux (t, j) handle SAME () => t end
 
-fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
+fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =
   let
     fun kill [] [] ts = foldr1 s_conj ts
       | kill (s :: ss) (T :: Ts) ts =
-        (case find_bound_assign thy stds (length ss) [] ts of
+        (case find_bound_assign ctxt stds (length ss) [] ts of
            SOME (_, []) => @{const True}
          | SOME (arg_t, ts) =>
            kill ss Ts (map (subst_one_bound (length ss)
@@ -893,7 +894,7 @@
       (if head_of t <> @{const "==>"} then add_def_axiom
        else add_nondef_axiom) depth t
     and add_eq_axiom depth t =
-      (if is_constr_pattern_formula thy t then add_def_axiom
+      (if is_constr_pattern_formula ctxt t then add_def_axiom
        else add_nondef_axiom) depth t
     and add_axioms_for_term depth t (accum as (xs, axs)) =
       case t of
@@ -921,7 +922,7 @@
                  fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
                       accum
                end
-             else if is_constr thy stds x then
+             else if is_constr ctxt stds x then
                accum
              else if is_equational_fun hol_ctxt x then
                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
@@ -929,7 +930,7 @@
              else if is_choice_spec_fun hol_ctxt x then
                fold (add_nondef_axiom depth)
                     (nondef_props_for_const thy true choice_spec_table x) accum
-             else if is_abs_fun thy x then
+             else if is_abs_fun ctxt x then
                if is_quot_type thy (range_type T) then
                  raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
                else
@@ -940,7 +941,7 @@
                           ? fold (add_maybe_def_axiom depth)
                                  (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
-             else if is_rep_fun thy x then
+             else if is_rep_fun ctxt x then
                if is_quot_type thy (domain_type T) then
                  raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
                else
@@ -952,9 +953,9 @@
                                  (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
                        |> add_axioms_for_term depth
-                                              (Const (mate_of_rep_fun thy x))
+                                              (Const (mate_of_rep_fun ctxt x))
                        |> fold (add_def_axiom depth)
-                               (inverse_axioms_for_rep_fun thy x)
+                               (inverse_axioms_for_rep_fun ctxt x)
              else if s = @{const_name TYPE} then
                accum
              else
@@ -979,8 +980,8 @@
       | TVar (_, S) => add_axioms_for_sort depth T S
       | Type (z as (_, Ts)) =>
         fold (add_axioms_for_type depth) Ts
-        #> (if is_pure_typedef thy T then
-              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+        #> (if is_pure_typedef ctxt T then
+              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
             else if is_quot_type thy T then
               fold (add_def_axiom depth)
                    (optimized_quot_type_axioms ctxt stds z)
@@ -1020,7 +1021,7 @@
 
 (** Simplification of constructor/selector terms **)
 
-fun simplify_constrs_and_sels thy t =
+fun simplify_constrs_and_sels ctxt t =
   let
     fun is_nth_sel_on t' n (Const (s, _) $ t) =
         (t = t' andalso is_sel_like_and_no_discr s andalso
@@ -1032,7 +1033,7 @@
                  $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
       | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
       | do_term (t as Const (x as (s, T))) (args as _ :: _) =
-        ((if is_constr_like thy x then
+        ((if is_constr_like ctxt x then
             if length args = num_binder_types T then
               case hd args of
                 Const (_, T') $ t' =>
@@ -1048,7 +1049,7 @@
           else if is_sel_like_and_no_discr s then
             case strip_comb (hd args) of
               (Const (x' as (s', T')), ts') =>
-              if is_constr_like thy x' andalso
+              if is_constr_like ctxt x' andalso
                  constr_name_for_sel_like s = s' andalso
                  not (exists is_pair_type (binder_types T')) then
                 list_comb (nth ts' (sel_no_from_name s), tl args)
@@ -1230,7 +1231,7 @@
 
 val max_skolem_depth = 4
 
-fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
+fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
                                   boxes, ...}) finitizes monos t =
   let
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
@@ -1250,7 +1251,7 @@
     val box = exists (not_equal (SOME false) o snd) boxes
     val table =
       Termtab.empty
-      |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
+      |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
     fun do_rest def =
       binarize ? binarize_nat_and_int_in_term
       #> box ? uncurry_term table
@@ -1261,7 +1262,7 @@
       #> curry_assms
       #> destroy_universal_equalities
       #> destroy_existential_equalities hol_ctxt
-      #> simplify_constrs_and_sels thy
+      #> simplify_constrs_and_sels ctxt
       #> distribute_quantifiers
       #> push_quantifiers_inward
       #> close_form
diff -r da728f9a68e8 -r 0dca1ec52999 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon May 31 18:51:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Jun 01 10:31:18 2010 +0200
@@ -135,7 +135,7 @@
    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
 
 fun quintuple_for_scope quote
-        ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
          datatypes, ...} : scope) =
   let
     val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@@ -144,8 +144,8 @@
       card_assigns |> filter_out (member (op =) boring_Ts o fst)
                    |> List.partition (is_fp_iterator_type o fst)
     val (secondary_card_assigns, primary_card_assigns) =
-      card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
-                                      o fst)
+      card_assigns
+      |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
     val cards =
       map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
                         string_of_int k)
@@ -458,13 +458,13 @@
      concrete = concrete, deep = deep, constrs = constrs}
   end
 
-fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize deep_dataTs
+fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
                           finitizable_dataTs (desc as (card_assigns, _)) =
   let
     val datatypes =
       map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
                                                finitizable_dataTs desc)
-          (filter (is_datatype thy stds o fst) card_assigns)
+          (filter (is_datatype ctxt stds o fst) card_assigns)
     val bits = card_of_type card_assigns @{typ signed_bit} - 1
                handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                       card_of_type card_assigns @{typ unsigned_bit}