src/ZF/Inductive.thy
changeset 24826 78e6a3cea367
parent 22814 4cd25f1706bb
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/Inductive.thy	Wed Oct 03 21:29:05 2007 +0200
     1.2 +++ b/src/ZF/Inductive.thy	Wed Oct 03 22:33:17 2007 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  structure Standard_Sum =
     1.6    struct
     1.7 -  val sum       = Const("op +", [iT,iT]--->iT)
     1.8 +  val sum       = Const(@{const_name sum}, [iT,iT]--->iT)
     1.9    val inl       = Const("Inl", iT-->iT)
    1.10    val inr       = Const("Inr", iT-->iT)
    1.11    val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)