src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 37678 0040bafffdef
parent 37476 0681e46b4022
child 37704 c6161bee8486
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -254,7 +254,7 @@
     1.4        else case T of
     1.5          Type (@{type_name fun}, [T1, T2]) =>
     1.6          MFun (fresh_mfun_for_fun_type mdata false T1 T2)
     1.7 -      | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
     1.8 +      | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
     1.9        | Type (z as (s, _)) =>
    1.10          if could_exist_alpha_sub_mtype ctxt alpha_T T then
    1.11            case AList.lookup (op =) (!datatype_mcache) z of
    1.12 @@ -1035,8 +1035,8 @@
    1.13            | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
    1.14              Type (if should_finitize T a then @{type_name fin_fun}
    1.15                    else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
    1.16 -          | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
    1.17 -            Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
    1.18 +          | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) =>
    1.19 +            Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2])
    1.20            | (MType _, _) => T
    1.21            | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
    1.22                                [M], [T])