src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 38126 8031d099379a
parent 37678 0040bafffdef
child 38170 d74b66ec02ce
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Jul 31 22:02:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Aug 01 15:51:25 2010 +0200
     1.3 @@ -902,8 +902,8 @@
     1.4      val all_values =
     1.5        all_values_of_type pool wacky_names scope atomss sel_names rel_table
     1.6                           bounds
     1.7 -    fun is_codatatype_wellformed (cos : dtype_spec list)
     1.8 -                                 ({typ, card, ...} : dtype_spec) =
     1.9 +    fun is_codatatype_wellformed (cos : datatype_spec list)
    1.10 +                                 ({typ, card, ...} : datatype_spec) =
    1.11        let
    1.12          val ts = all_values card typ
    1.13          val max_depth = Integer.sum (map #card cos)
    1.14 @@ -935,7 +935,7 @@
    1.15              [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
    1.16               Pretty.str oper, Syntax.pretty_term ctxt t2])
    1.17        end
    1.18 -    fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
    1.19 +    fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
    1.20        Pretty.block (Pretty.breaks
    1.21            (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
    1.22             (case typ of
    1.23 @@ -950,8 +950,8 @@
    1.24                    else [Pretty.str (unrep ())]))]))
    1.25      fun integer_datatype T =
    1.26        [{typ = T, card = card_of_type card_assigns T, co = false,
    1.27 -        standard = true, complete = (false, false), concrete = (true, true),
    1.28 -        deep = true, constrs = []}]
    1.29 +        standard = true, self_rec = true, complete = (false, false),
    1.30 +        concrete = (true, true), deep = true, constrs = []}]
    1.31        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    1.32      val (codatatypes, datatypes) =
    1.33        datatypes |> filter #deep |> List.partition #co