| changeset 22781 | 18fbba942a80 |
| parent 22633 | a47e4fd7ebc1 |
| child 24019 | 67bde7cfcf10 |
--- a/src/HOL/Bali/Basis.thy Tue Apr 24 15:15:52 2007 +0200 +++ b/src/HOL/Bali/Basis.thy Tue Apr 24 15:17:22 2007 +0200 @@ -216,7 +216,7 @@ syntax fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80) translations - "fun_sum" == "sum_case" + "fun_sum" == "CONST sum_case" consts the_Inl :: "'a + 'b \<Rightarrow> 'a" the_Inr :: "'a + 'b \<Rightarrow> 'b"