# HG changeset patch
# User wenzelm
# Date 1526834718 -7200
# Node ID 5e0e9376b2b045b091997b6efee00efcb02d48bd
# Parent  4b93573ac5b4023570fdcd8a530f56fb2c6eab42
avoid undeclared frees;

diff -r 4b93573ac5b4 -r 5e0e9376b2b0 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/Bin.thy	Sun May 20 18:45:18 2018 +0200
@@ -652,15 +652,6 @@
 
 (** For cancel_numerals **)
 
-lemmas rel_iff_rel_0_rls =
-  zless_iff_zdiff_zless_0 [where y = "u $+ v"]
-  eq_iff_zdiff_eq_0 [where y = "u $+ v"]
-  zle_iff_zdiff_zle_0 [where y = "u $+ v"]
-  zless_iff_zdiff_zless_0 [where y = n]
-  eq_iff_zdiff_eq_0 [where y = n]
-  zle_iff_zdiff_zle_0 [where y = n]
-  for u v (* FIXME n (!?) *)
-
 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
@@ -673,6 +664,18 @@
   apply (simp add: zadd_ac)
   done
 
+context fixes n :: i
+begin
+
+lemmas rel_iff_rel_0_rls =
+  zless_iff_zdiff_zless_0 [where y = "u $+ v"]
+  eq_iff_zdiff_eq_0 [where y = "u $+ v"]
+  zle_iff_zdiff_zle_0 [where y = "u $+ v"]
+  zless_iff_zdiff_zless_0 [where y = n]
+  eq_iff_zdiff_eq_0 [where y = n]
+  zle_iff_zdiff_zle_0 [where y = n]
+  for u v
+
 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
@@ -681,6 +684,8 @@
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
+end
+
 lemma le_add_iff1: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $\<le> n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
diff -r 4b93573ac5b4 -r 5e0e9376b2b0 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy	Sun May 20 18:45:18 2018 +0200
@@ -22,7 +22,7 @@
     tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1]
   and forest'induct =
     tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1]
-  for t
+  for t f
 
 declare tree_forest.intros [simp, TC]
 
diff -r 4b93573ac5b4 -r 5e0e9376b2b0 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Sun May 20 18:45:18 2018 +0200
@@ -451,7 +451,7 @@
 
 (*Delete the nearest invariance assumption (which will be the second one
   used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
+lemmas Always_thin = thin_rl [of "F \<in> Always(A)"] for F A
 
 (*To allow expansion of the program's definition when appropriate*)
 named_theorems program "program definitions"
diff -r 4b93573ac5b4 -r 5e0e9376b2b0 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/upair.thy	Sun May 20 18:45:18 2018 +0200
@@ -230,10 +230,10 @@
 **)
 
 lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
-lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
+lemmas split_if_eq2 = split_if [of "%x. a = x"] for a
 
 lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
-lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x
+lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for a
 
 lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2