# HG changeset patch
# User wenzelm
# Date 1159479763 -7200
# Node ID 2c583720436e7b017d589373c43d94ba86ee8a69
# Parent  5d538d3d5e2afda4c97b80aa0fa46e9505e7082a
fixed translations: CONST;

diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -255,7 +255,7 @@
   array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
 translations
   "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
-  "a[i] := v" => "(i < length a) \<rightarrow> (a := list_update a i v)"
+  "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
   (* reverse translation not possible because of duplicate "a" *)
 
 text{* Note: there is no special syntax for guarded array access. Thus
diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -27,7 +27,7 @@
 syntax
   "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
 translations
-  "\<Sum>i. b" == "suminf (%i. b)"
+  "\<Sum>i. b" == "CONST suminf (%i. b)"
 
 
 lemma sumr_diff_mult_const:
diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Induct/LList.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -95,8 +95,11 @@
 
 
 text{* The case syntax for type @{text "'a llist"} *}
+syntax  (* FIXME proper case syntax!? *)
+  LNil :: logic
+  LCons :: logic
 translations
-  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
+  "case p of LNil => a | LCons x l => b" == "CONST llist_case a (%x l. b) p"
 
 
 subsubsection{* Sample function definitions.  Item-based ones start with @{text L} *}
diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Induct/SList.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -73,7 +73,7 @@
 (*Declaring the abstract list constructors*)
 
 definition
-  Nil       :: "'a list"
+  Nil       :: "'a list"                               ("[]")
    "Nil  = Abs_List(NIL)"
 
   "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
@@ -88,19 +88,16 @@
    "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
 
 (* list Enumeration *)
-consts
-  "[]"      :: "'a list"                            ("[]")
 syntax
   "@list"   :: "args => 'a list"                    ("[(_)]")
 
 translations
   "[x, xs]" == "x#[xs]"
   "[x]"     == "x#[]"
-  "[]"      == "Nil"
 
-  "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys. b, xs)"
+  "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
 
-  
+
 (* *********************************************************************** *)
 (*                                                                         *)
 (* Generalized Map Functionals                                             *)
@@ -205,8 +202,8 @@
   "@filter"     :: "[idt, 'a list, bool] => 'a list"     ("(1[_:_ ./ _])")
 
 translations
-  "[x:xs. P]"   == "filter(%x. P) xs"
-  "Alls x:xs. P"== "list_all(%x. P)xs"
+  "[x:xs. P]" == "CONST filter(%x. P) xs"
+  "Alls x:xs. P" == "CONST list_all(%x. P)xs"
 
 
 lemma ListI: "x : list (range Leaf) ==> x : List"
diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -196,8 +196,12 @@
 definition
   "llist_case c d l =
     List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
+
+syntax  (* FIXME? *)
+  LNil :: logic
+  LCons :: logic
 translations
-  "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "llist_case a (\<lambda>x l. b) p"
+  "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
 
 lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
   by (simp add: llist_case_def LNil_def
diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -39,8 +39,8 @@
   "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
 translations
-  "PI x:A. B" == "Pi A (%x. B)"
-  "%x:A. f" == "restrict (%x. f) A"
+  "PI x:A. B" == "CONST Pi A (%x. B)"
+  "%x:A. f" == "CONST restrict (%x. f) A"
 
 definition
   "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
diff -r 5d538d3d5e2a -r 2c583720436e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -40,7 +40,7 @@
 syntax
   "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
 translations
-  "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
+  "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)"
 
 definition
   set_of :: "'a multiset => 'a set"
diff -r 5d538d3d5e2a -r 2c583720436e src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOLCF/Porder.thy	Thu Sep 28 23:42:43 2006 +0200
@@ -94,7 +94,7 @@
   "LUB "	:: "[idts, 'a] \<Rightarrow> 'a"		("(3\<Squnion>_./ _)" [0,10] 10)
 
 translations
-  "\<Squnion>n. t" == "lub(range(\<lambda>n. t))"
+  "\<Squnion>n. t" == "lub(CONST range(\<lambda>n. t))"
 
 text {* lubs are unique *}