src/HOL/Bali/Basis.thy
changeset 33965 f57c11db4ad4
parent 32960 69916a850301
child 34915 7894c7dab132
     1.1 --- a/src/HOL/Bali/Basis.thy	Fri Nov 27 08:42:34 2009 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Fri Nov 27 08:42:50 2009 +0100
     1.3 @@ -216,8 +216,8 @@
     1.4           In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
     1.5           In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
     1.6  translations
     1.7 -        "In1l e" == "In1 (Inl e)"
     1.8 -        "In1r c" == "In1 (Inr c)"
     1.9 +        "In1l e" == "In1 (CONST Inl e)"
    1.10 +        "In1r c" == "In1 (CONST Inr c)"
    1.11  
    1.12  syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
    1.13         the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
    1.14 @@ -233,7 +233,7 @@
    1.15  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    1.16  
    1.17  translations
    1.18 -  "option"<= (type) "Datatype.option"
    1.19 +  "option"<= (type) "Option.option"
    1.20    "list"  <= (type) "List.list"
    1.21    "sum3"  <= (type) "Basis.sum3"
    1.22