src/HOL/Tools/datatype_rep_proofs.ML
changeset 15391 797ed46d724b
parent 14981 e73f8140af78
child 15457 1fbd4aba46e3
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 09 15:49:40 2004 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 09 16:45:46 2004 +0100
     1.3 @@ -103,9 +103,9 @@
     1.4                val Type (_, [T1, T2]) = T
     1.5            in
     1.6              if i <= n2 then
     1.7 -              Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
     1.8 +              Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i)
     1.9              else
    1.10 -              Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
    1.11 +              Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
    1.12            end
    1.13        in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
    1.14        end;