src/HOL/Tools/inductive_package.ML
changeset 15391 797ed46d724b
parent 15032 02aed07e01bf
child 15416 db69af736ebb
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 09 15:49:40 2004 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 09 16:45:46 2004 +0100
     1.3 @@ -212,9 +212,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 cs) (1 + find_index_eq c cs)
    1.14    end;