--- a/thys2/Recs.thy	Mon Jan 07 13:44:19 2019 +0100
+++ b/thys2/Recs.thy	Thu Jan 10 12:48:43 2019 +0000
@@ -1,6 +1,6 @@
 theory Recs
-imports Main Fact 
-        "~~/src/HOL/Number_Theory/Primes" 
+  imports Main
+        "~~/src/HOL/Number_Theory/Primes"  
         "~~/src/HOL/Library/Nat_Bijection"
         "~~/src/HOL/Library/Discrete"
 begin
@@ -45,8 +45,8 @@
 
 lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
   setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
-apply(subst setsum_Un_disjoint[symmetric])
-apply(auto simp add: ivl_disj_un_one)
+  apply(subst setsum.union_disjoint[symmetric])
+  apply(auto simp add: ivl_disj_un_one)
 done
 
 lemma setsum_eq_zero [simp]:
@@ -249,10 +249,10 @@
   "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
 
 definition 
-  "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
+  "rec_predi = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
 definition 
-  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
+  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_predi [Id 3 1]))"
 
 lemma constn_lemma [simp]: 
   "rec_eval (constn n) xs = n"
@@ -283,8 +283,8 @@
 by (simp add: rec_fact_def)
 
 lemma pred_lemma [simp]: 
-  "rec_eval rec_pred [x] =  x - 1"
-by (induct x) (simp_all add: rec_pred_def)
+  "rec_eval rec_predi [x] =  x - 1"
+by (induct x) (simp_all add: rec_predi_def)
 
 lemma minus_lemma [simp]: 
   "rec_eval rec_minus [x, y] = x - y"
@@ -823,13 +823,13 @@
 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]"
 
 definition 
-  "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
+  "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
 
 definition 
   "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
 
 definition
-  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]"
+  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]"
 
 lemma ldec_iter:
   "ldec z n = pdec1 (Iter pdec2 n z) - 1"