1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Feb 02 11:38:38 2010 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Tools/Nitpick/nitpick_kodkod.ML
     1.5      Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2008, 2009
     1.7 +    Copyright   2008, 2009, 2010
     1.8  
     1.9  Kodkod problem generator part of Kodkod.
    1.10  *)
    1.11 @@ -285,8 +285,8 @@
    1.12  (* Proof.context -> bool -> string -> typ -> rep -> string *)
    1.13  fun bound_comment ctxt debug nick T R =
    1.14    short_name nick ^
    1.15 -  (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
    1.16 -   else "") ^ " : " ^ string_for_rep R
    1.17 +  (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
    1.18 +  " : " ^ string_for_rep R
    1.19  
    1.20  (* Proof.context -> bool -> nut -> KK.bound *)
    1.21  fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
    1.22 @@ -754,7 +754,7 @@
    1.23  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    1.24     -> dtype_spec -> nfa_entry option *)
    1.25  fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    1.26 -  | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
    1.27 +  | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
    1.28    | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
    1.29      SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
    1.30                       o #const) constrs)
    1.31 @@ -926,7 +926,7 @@
    1.32  
    1.33  (* extended_context -> int -> int Typtab.table -> kodkod_constrs
    1.34     -> nut NameTable.table -> dtype_spec -> KK.formula list *)
    1.35 -fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
    1.36 +fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
    1.37    | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
    1.38                                (dtype as {typ, ...}) =
    1.39      let val j0 = offset_of_type ofs typ in