src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 41052 3db267a01c1d
parent 41039 405a9f41ad6b
child 41472 f6ab14e61604
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -178,9 +178,7 @@
     1.4  fun tuple_list_for_name rel_table bounds name =
     1.5    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
     1.6  
     1.7 -fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
     1.8 -    unarize_unbox_etc_term t1
     1.9 -  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    1.10 +fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    1.11      unarize_unbox_etc_term t1
    1.12    | unarize_unbox_etc_term
    1.13          (Const (@{const_name PairBox},
    1.14 @@ -559,9 +557,8 @@
    1.15                    if length arg_Ts = 0 then
    1.16                      []
    1.17                    else
    1.18 -                    map3 (fn Ts =>
    1.19 -                             term_for_rep (constr_s <> @{const_name FinFun})
    1.20 -                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
    1.21 +                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
    1.22 +                         arg_jsss
    1.23                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
    1.24                      |> dest_n_tuple (length uncur_arg_Ts)
    1.25                  val t =
    1.26 @@ -935,8 +932,7 @@
    1.27        Pretty.block (Pretty.breaks
    1.28            (pretty_for_type ctxt typ ::
    1.29             (case typ of
    1.30 -              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
    1.31 -            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
    1.32 +              Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
    1.33              | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
    1.34              | _ => []) @
    1.35             [Pretty.str "=",