# HG changeset patch
# User wenzelm
# Date 1526846686 -7200
# Node ID eb57621568bb001175ffaa5e160e92fd89e3e6ac
# Parent  e7c85e2dc1988646a33c069e91c6a59b3fa6c572
avoid undeclared frees;

diff -r e7c85e2dc198 -r eb57621568bb src/Doc/Tutorial/Rules/Forward.thy
--- a/src/Doc/Tutorial/Rules/Forward.thy	Sun May 20 22:04:17 2018 +0200
+++ b/src/Doc/Tutorial/Rules/Forward.thy	Sun May 20 22:04:46 2018 +0200
@@ -55,14 +55,14 @@
 \<close>
 
 
-lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
+lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] for k
 lemmas gcd_mult_1 = gcd_mult_0 [simplified]
 
 lemmas where1 = gcd_mult_distrib2 [where m=1]
 
 lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1]
 
-lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"]
+lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] for j k
 
 text \<open>
 example using ``of'':
@@ -87,7 +87,7 @@
 lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
       (*not quite right: we need ?k but this gives k*)
 
-lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
+lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] for k
       (*better in one step!*)
 
 text \<open>
@@ -98,7 +98,7 @@
 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
 
 
-lemmas gcd_self0 = gcd_mult [of k 1, simplified]
+lemmas gcd_self0 = gcd_mult [of k 1, simplified] for k
 
 
 text \<open>
diff -r e7c85e2dc198 -r eb57621568bb src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Sun May 20 22:04:17 2018 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Sun May 20 22:04:46 2018 +0200
@@ -387,7 +387,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
 
 
 subsection\<open>Totalize\<close>