diff -r eed7ca453573 -r 3c9a0985e6be src/CCL/Term.thy
--- a/src/CCL/Term.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/CCL/Term.thy	Mon Jan 11 21:16:38 2016 +0100
@@ -9,48 +9,69 @@
 imports CCL
 begin
 
-consts
+definition one :: "i"
+  where "one == true"
 
-  one        :: "i"
+definition "if" :: "[i,i,i]\<Rightarrow>i"  ("(3if _/ then _/ else _)" [0,0,60] 60)
+  where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
-  "if"       :: "[i,i,i]\<Rightarrow>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
+definition inl :: "i\<Rightarrow>i"
+  where "inl(a) == <true,a>"
 
-  inl        :: "i\<Rightarrow>i"
-  inr        :: "i\<Rightarrow>i"
-  "when"     :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+definition inr :: "i\<Rightarrow>i"
+  where "inr(b) == <false,b>"
+
+definition split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
 
-  split      :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
-  fst        :: "i\<Rightarrow>i"
-  snd        :: "i\<Rightarrow>i"
-  thd        :: "i\<Rightarrow>i"
+definition "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
+
+definition fst :: "i\<Rightarrow>i"
+  where "fst(t) == split(t, \<lambda>x y. x)"
 
-  zero       :: "i"
-  succ       :: "i\<Rightarrow>i"
-  ncase      :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
-  nrec       :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition snd :: "i\<Rightarrow>i"
+  where "snd(t) == split(t, \<lambda>x y. y)"
+
+definition thd :: "i\<Rightarrow>i"
+  where "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
+
+definition zero :: "i"
+  where "zero == inl(one)"
 
-  nil        :: "i"                        ("([])")
-  cons       :: "[i,i]\<Rightarrow>i"                 (infixr "$" 80)
-  lcase      :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
-  lrec       :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition succ :: "i\<Rightarrow>i"
+  where "succ(n) == inr(n)"
+
+definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
 
-  "let"      :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
-  letrec     :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  letrec2    :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  letrec3    :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+
+no_syntax
+  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+
+definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
 syntax
-  "_let"     :: "[id,i,i]\<Rightarrow>i"             ("(3let _ be _/ in _)"
-                        [0,0,60] 60)
+  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
 
-  "_letrec"  :: "[id,id,i,i]\<Rightarrow>i"         ("(3letrec _ _ be _/ in _)"
-                        [0,0,0,60] 60)
+definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+
+definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec2 (h, f) ==
+    letrec (\<lambda>p g'. split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>))), \<lambda>g'. f(\<lambda>x y. g'(<x,y>)))"
 
-  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"     ("(3letrec _ _ _ be _/ in _)"
-                        [0,0,0,0,60] 60)
+definition letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec3 (h, f) ==
+    letrec (\<lambda>p g'. split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>)))),
+      \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
-  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)"
-                        [0,0,0,0,0,60] 60)
+syntax
+  "_let" :: "[id,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+  "_letrec" :: "[id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
 
 ML \<open>
 (** Quantifier translations: variable binding **)
@@ -107,42 +128,24 @@
   (@{const_syntax letrec3}, K letrec3_tr')]
 \<close>
 
-consts
-  napply     :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
+
+definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
+
+definition nil :: "i"  ("([])")
+  where "[] == inl(one)"
 
-defs
-  one_def:                    "one == true"
-  if_def:     "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
-  inl_def:                 "inl(a) == <true,a>"
-  inr_def:                 "inr(b) == <false,b>"
-  when_def:           "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
-  split_def:           "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
-  fst_def:                 "fst(t) == split(t, \<lambda>x y. x)"
-  snd_def:                 "snd(t) == split(t, \<lambda>x y. y)"
-  thd_def:                 "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
-  zero_def:                  "zero == inl(one)"
-  succ_def:               "succ(n) == inr(n)"
-  ncase_def:         "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
-  nrec_def:          " nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
-  nil_def:                     "[] == inl(one)"
-  cons_def:                   "h$t == inr(<h,t>)"
-  lcase_def:         "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
-  lrec_def:           "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
+definition cons :: "[i,i]\<Rightarrow>i"  (infixr "$" 80)
+  where "h$t == inr(<h,t>)"
+
+definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
 
-  let_def:  "let x be t in f(x) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-  letrec_def:
-  "letrec g x be h(x,g) in b(g) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
-  letrec2_def:  "letrec g x y be h(x,y,g) in f(g)==
-               letrec g' p be split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>)))
-                          in f(\<lambda>x y. g'(<x,y>))"
-
-  letrec3_def:  "letrec g x y z be h(x,y,z,g) in f(g) ==
-             letrec g' p be split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>))))
-                          in f(\<lambda>x y z. g'(<x,<y,z>>))"
-
-  napply_def: "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
-
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  ("(_ ^ _ ` _)" [56,56,56] 56)
+  where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
   and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def