--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 09 15:49:40 2004 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 09 16:45:46 2004 +0100
@@ -103,9 +103,9 @@
val Type (_, [T1, T2]) = T
in
if i <= n2 then
- Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
+ Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i)
else
- Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+ Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
end
in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
end;