# HG changeset patch
# User wenzelm
# Date 1181855076 -7200
# Node ID 31781b2de73da5176096b5c20cca6d852e5d6eaf
# Parent  4b03e3586f7f6c2f418bc72ff4acef258845e9ba
tuned proofs: avoid implicit prems;

diff -r 4b03e3586f7f -r 31781b2de73d src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/FOL/IFOL.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -319,27 +319,23 @@
 ***)
 
 lemma ex1I:
-  assumes "P(a)"
-    and "!!x. P(x) ==> x=a"
-  shows "EX! x. P(x)"
+  "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
   apply (unfold ex1_def)
-  apply (assumption | rule assms exI conjI allI impI)+
+  apply (assumption | rule exI conjI allI impI)+
   done
 
 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
 lemma ex_ex1I:
-  assumes ex: "EX x. P(x)"
-    and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
-  shows "EX! x. P(x)"
-  apply (rule ex [THEN exE])
-  apply (assumption | rule ex1I eq)+
+  "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
+  apply (erule exE)
+  apply (rule ex1I)
+   apply assumption
+  apply assumption
   done
 
 lemma ex1E:
-  assumes ex1: "EX! x. P(x)"
-    and r: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
-  shows R
-  apply (insert ex1, unfold ex1_def)
+  "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
+  apply (unfold ex1_def)
   apply (assumption | erule exE conjE)+
   done
 
@@ -572,11 +568,11 @@
 (*Simplifies the implication.  Classical version is stronger. 
   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
 lemma not_impE:
-  assumes major: "~P --> S"
-    and r1: "P ==> False"
-    and r2: "S ==> R"
-  shows R
-  apply (assumption | rule notI impI major [THEN mp] r1 r2)+
+  "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
+  apply (drule mp)
+   apply (rule notI)
+   apply assumption
+  apply assumption
   done
 
 (*Simplifies the implication.   UNSAFE.  *)
@@ -595,7 +591,7 @@
     and r1: "!!x. P(x)"
     and r2: "S ==> R"
   shows R
-  apply (assumption | rule allI impI major [THEN mp] r1 r2)+
+  apply (rule allI impI major [THEN mp] r1 r2)+
   done
 
 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
@@ -609,10 +605,8 @@
 (*** Courtesy of Krzysztof Grabczewski ***)
 
 lemma disj_imp_disj:
-  assumes major: "P|Q"
-    and "P==>R" and "Q==>S"
-  shows "R|S"
-  apply (rule disjE [OF major])
+  "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
+  apply (erule disjE)
   apply (rule disjI1) apply assumption
   apply (rule disjI2) apply assumption
   done
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -22,7 +22,7 @@
 lemma I: "A --> A"
 proof
   assume A
-  show A by assumption
+  show A by fact
 qed
 
 lemma K: "A --> B --> A"
@@ -30,7 +30,7 @@
   assume A
   show "B --> A"
   proof
-    show A by assumption
+    show A by fact
   qed
 qed
 
@@ -45,8 +45,8 @@
       assume A
       show C
       proof (rule mp)
-        show "B --> C" by (rule mp) assumption+
-        show B by (rule mp) assumption+
+        show "B --> C" by (rule mp) fact+
+        show B by (rule mp) fact+
       qed
     qed
   qed
@@ -65,7 +65,7 @@
 lemma "A --> A"
 proof
   assume A
-  show A by assumption
+  show A by fact+
 qed
 
 text {*
@@ -117,7 +117,7 @@
 lemma "A --> B --> A"
 proof (intro impI)
   assume A
-  show A by assumption
+  show A by fact
 qed
 
 text {*
@@ -162,8 +162,8 @@
   assume "A & B"
   show "B & A"
   proof
-    show B by (rule conjunct2) assumption
-    show A by (rule conjunct1) assumption
+    show B by (rule conjunct2) fact
+    show A by (rule conjunct1) fact
   qed
 qed
 
@@ -294,9 +294,9 @@
   proof                    -- {*
     rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   *}
-    assume P show P by assumption
+    assume P show P by fact
   next
-    assume P show P by assumption
+    assume P show P by fact
   qed
 qed
 
@@ -330,8 +330,8 @@
   then show P
   proof
     assume P
-    show P by assumption
-    show P by assumption
+    show P by fact
+    show P by fact
   qed
 qed
 
@@ -439,8 +439,8 @@
   assume r: "A ==> B ==> C"
   show C
   proof (rule r)
-    show A by (rule conjunct1) assumption
-    show B by (rule conjunct2) assumption
+    show A by (rule conjunct1) fact
+    show B by (rule conjunct2) fact
   qed
 qed
 
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Lattice/Bounds.thy
--- a/src/HOL/Lattice/Bounds.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Lattice/Bounds.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -193,8 +193,8 @@
   show ?thesis
   proof
     show "x \<sqsubseteq> x" ..
-    show "x \<sqsubseteq> y" by assumption
-    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by assumption
+    show "x \<sqsubseteq> y" by fact
+    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
   qed
 qed
 
@@ -203,10 +203,10 @@
   assume "x \<sqsubseteq> y"
   show ?thesis
   proof
-    show "x \<sqsubseteq> y" by assumption
+    show "x \<sqsubseteq> y" by fact
     show "y \<sqsubseteq> y" ..
     fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
-    show "y \<sqsubseteq> z" by assumption
+    show "y \<sqsubseteq> z" by fact
   qed
 qed
 
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -232,7 +232,7 @@
   show "x \<sqsubseteq> x" ..
   show "x \<sqsubseteq> x \<squnion> y" ..
   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
-  show "z \<sqsubseteq> x" by assumption
+  show "z \<sqsubseteq> x" by fact
 qed
 
 theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -24,7 +24,7 @@
   ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp
 next
   case (Lam z M)
-  have vc: "z\<sharp>x" "z\<sharp>P" by fact
+  have vc: "z\<sharp>x" "z\<sharp>P" by fact+
   have ih: "x\<sharp>M \<Longrightarrow>  M[x::=P] = M" by fact
   have asm: "x\<sharp>Lam [z].M" by fact
   then have "x\<sharp>M" using vc by (simp add: fresh_atm abs_fresh)
@@ -46,7 +46,7 @@
 using asms
 proof (nominal_induct N avoiding: z y L rule: lam.induct)
   case (Var u)
-  have "z\<sharp>(Var u)" "z\<sharp>L" by fact
+  have "z\<sharp>(Var u)" "z\<sharp>L" by fact+
   thus "z\<sharp>((Var u)[y::=L])" by simp
 next
   case (App N1 N2)
@@ -54,11 +54,11 @@
   moreover
   have ih2: "\<lbrakk>z\<sharp>N2; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N2[y::=L]" by fact
   moreover 
-  have "z\<sharp>App N1 N2" "z\<sharp>L" by fact
+  have "z\<sharp>App N1 N2" "z\<sharp>L" by fact+
   ultimately show "z\<sharp>((App N1 N2)[y::=L])" by simp 
 next
   case (Lam u N1)
-  have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact 
+  have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact+
   have "z\<sharp>Lam [u].N1" by fact
   hence "z\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm)
   moreover
@@ -123,7 +123,7 @@
   have ih: "\<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
   have "x\<noteq>y" by fact
   have "x\<sharp>L" by fact
-  have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
+  have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact+
   hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
   show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
   proof - 
@@ -334,7 +334,7 @@
 using a
 proof (nominal_induct M avoiding: x N N' rule: lam.induct)
   case (Var y) 
-  show "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
+  thus "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y") auto
 next
   case (App P Q) (* application case - third line *)
   thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1  (App P Q)[x::=N']" using o2 by simp
@@ -367,7 +367,7 @@
   thus ?case by simp
 next
   case (o4 a N1 N2 M1 M2 N N' x)
-  have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact
+  have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact+
   have asm: "N\<longrightarrow>\<^isub>1N'" by fact
   show ?case
   proof -
@@ -401,7 +401,7 @@
   thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3" by blast
 next
   case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
-  have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact
+  have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact+
   have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact
@@ -559,8 +559,8 @@
   case o3 thus ?case by (blast intro!: one_lam_cong)
 next 
   case (o4 a s1 s2 t1 t2)
-  have vc: "a\<sharp>s1" "a\<sharp>s2" by fact
-  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact
+  have vc: "a\<sharp>s1" "a\<sharp>s2" by fact+
+  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact+
   have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4)
   from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
     by (blast intro!: one_app_cong one_lam_cong)
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -5878,7 +5878,7 @@
   qed
 next
   case (Cut b M z N x a y)
-  have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>N" "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>M" by fact
+  have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>N" "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>M" by fact+
   have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
   show "(Cut <b>.M (z).N){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (Cut <b>.M (z).N)[x\<turnstile>n>y]"
@@ -5900,14 +5900,14 @@
   qed
 next
   case (NotR z M b x a y)
-  have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>b" by fact
+  have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "z\<sharp>b" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have "(NotR (z).M b){x:=<a>.Ax y a} = NotR (z).(M{x:=<a>.Ax y a}) b" using fs by simp
   also have "\<dots> \<longrightarrow>\<^isub>a* NotR (z).(M[x\<turnstile>n>y]) b" using ih by (auto intro: a_star_congs)
   finally show "(NotR (z).M b){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (NotR (z).M b)[x\<turnstile>n>y]" using fs by simp
 next
   case (NotL b M z x a y)  
-  have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>z" by fact
+  have fs: "b\<sharp>x" "b\<sharp>a" "b\<sharp>y" "b\<sharp>z" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   show "(NotL <b>.M z){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (NotL <b>.M z)[x\<turnstile>n>y]"
   proof(cases "z=x")
@@ -5939,7 +5939,7 @@
   qed
 next
   case (AndR c M d N e x a y)
-  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "d\<sharp>x" "d\<sharp>a" "d\<sharp>y" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact
+  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "d\<sharp>x" "d\<sharp>a" "d\<sharp>y" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact+
   have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
   have "(AndR <c>.M <d>.N e){x:=<a>.Ax y a} = AndR <c>.(M{x:=<a>.Ax y a}) <d>.(N{x:=<a>.Ax y a}) e"
@@ -5949,7 +5949,7 @@
     using fs by simp
 next
   case (AndL1 u M v x a y)
-  have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact
+  have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   show "(AndL1 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (AndL1 (u).M v)[x\<turnstile>n>y]"
   proof(cases "v=x")
@@ -5983,7 +5983,7 @@
   qed
 next
   case (AndL2 u M v x a y)
-  have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact
+  have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "u\<sharp>v" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   show "(AndL2 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (AndL2 (u).M v)[x\<turnstile>n>y]"
   proof(cases "v=x")
@@ -6017,21 +6017,21 @@
   qed
 next
   case (OrR1 c M d  x a y)
-  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact
+  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have "(OrR1 <c>.M d){x:=<a>.Ax y a} = OrR1 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
   also have "\<dots> \<longrightarrow>\<^isub>a* OrR1 <c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs)
   finally show "(OrR1 <c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (OrR1 <c>.M d)[x\<turnstile>n>y]" using fs by simp
 next
   case (OrR2 c M d  x a y)
-  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact
+  have fs: "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "c\<sharp>d" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have "(OrR2 <c>.M d){x:=<a>.Ax y a} = OrR2 <c>.(M{x:=<a>.Ax y a}) d" using fs by (simp add: fresh_atm)
   also have "\<dots> \<longrightarrow>\<^isub>a* OrR2 <c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs)
   finally show "(OrR2 <c>.M d){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (OrR2 <c>.M d)[x\<turnstile>n>y]" using fs by simp
 next
   case (OrL u M v N z x a y)
-  have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "v\<sharp>x" "v\<sharp>a" "v\<sharp>y" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact
+  have fs: "u\<sharp>x" "u\<sharp>a" "u\<sharp>y" "v\<sharp>x" "v\<sharp>a" "v\<sharp>y" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact+
   have ih1: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have ih2: "N{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* N[x\<turnstile>n>y]" by fact
   show "(OrL (u).M (v).N z){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (OrL (u).M (v).N z)[x\<turnstile>n>y]"
@@ -6070,7 +6070,7 @@
   qed
 next
   case (ImpR z c M d x a y)
-  have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "z\<sharp>d" "c\<sharp>d" by fact
+  have fs: "z\<sharp>x" "z\<sharp>a" "z\<sharp>y" "c\<sharp>x" "c\<sharp>a" "c\<sharp>y" "z\<sharp>d" "c\<sharp>d" by fact+
   have ih: "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]" by fact
   have "(ImpR (z).<c>.M d){x:=<a>.Ax y a} = ImpR (z).<c>.(M{x:=<a>.Ax y a}) d" using fs by simp
   also have "\<dots> \<longrightarrow>\<^isub>a* ImpR (z).<c>.(M[x\<turnstile>n>y]) d" using ih by (auto intro: a_star_congs)
@@ -6135,7 +6135,7 @@
   qed
 next
   case (Cut c M z N b a x)
-  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>N" "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>M" by fact
+  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>N" "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>M" by fact+
   have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
   show "(Cut <c>.M (z).N){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (Cut <c>.M (z).N)[b\<turnstile>c>a]"
@@ -6157,7 +6157,7 @@
   qed
 next
   case (NotR z M c b a x)
-  have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>c" by fact
+  have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "z\<sharp>c" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   show "(NotR (z).M c){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (NotR (z).M c)[b\<turnstile>c>a]"
   proof (cases "c=b")
@@ -6190,14 +6190,14 @@
   qed
 next
   case (NotL c M z b a x)  
-  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>z" by fact
+  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>z" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have "(NotL <c>.M z){b:=(x).Ax x a} = NotL <c>.(M{b:=(x).Ax x a}) z" using fs by simp
   also have "\<dots> \<longrightarrow>\<^isub>a* NotL <c>.(M[b\<turnstile>c>a]) z" using ih by (auto intro: a_star_congs)
   finally show "(NotL <c>.M z){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (NotL <c>.M z)[b\<turnstile>c>a]" using fs by simp
 next
   case (AndR c M d N e b a x)
-  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "d\<sharp>b" "d\<sharp>a" "d\<sharp>x" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact
+  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "d\<sharp>b" "d\<sharp>a" "d\<sharp>x" "d\<noteq>c" "c\<sharp>N" "c\<sharp>e" "d\<sharp>M" "d\<sharp>e" by fact+
   have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
   show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (AndR <c>.M <d>.N e)[b\<turnstile>c>a]"
@@ -6235,21 +6235,21 @@
   qed
 next
   case (AndL1 u M v b a x)
-  have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact
+  have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have "(AndL1 (u).M v){b:=(x).Ax x a} = AndL1 (u).(M{b:=(x).Ax x a}) v" using fs by simp
   also have "\<dots> \<longrightarrow>\<^isub>a* AndL1 (u).(M[b\<turnstile>c>a]) v" using ih by (auto intro: a_star_congs)
   finally show "(AndL1 (u).M v){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (AndL1 (u).M v)[b\<turnstile>c>a]" using fs by simp
 next
   case (AndL2 u M v b a x)
-  have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact
+  have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "u\<sharp>v" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have "(AndL2 (u).M v){b:=(x).Ax x a} = AndL2 (u).(M{b:=(x).Ax x a}) v" using fs by simp
   also have "\<dots> \<longrightarrow>\<^isub>a* AndL2 (u).(M[b\<turnstile>c>a]) v" using ih by (auto intro: a_star_congs)
   finally show "(AndL2 (u).M v){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (AndL2 (u).M v)[b\<turnstile>c>a]" using fs by simp
 next
   case (OrR1 c M d  b a x)
-  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact
+  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   show "(OrR1 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (OrR1 <c>.M d)[b\<turnstile>c>a]"
   proof(cases "d=b")
@@ -6283,7 +6283,7 @@
   qed
 next
   case (OrR2 c M d  b a x)
-  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact
+  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "c\<sharp>d" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   show "(OrR2 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (OrR2 <c>.M d)[b\<turnstile>c>a]"
   proof(cases "d=b")
@@ -6317,7 +6317,7 @@
   qed
 next
   case (OrL u M v N z b a x)
-  have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "v\<sharp>b" "v\<sharp>a" "v\<sharp>x" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact
+  have fs: "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "v\<sharp>b" "v\<sharp>a" "v\<sharp>x" "v\<noteq>u" "u\<sharp>N" "u\<sharp>z" "v\<sharp>M" "v\<sharp>z" by fact+
   have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
   have "(OrL (u).M (v).N z){b:=(x).Ax x a} = OrL (u).(M{b:=(x).Ax x a}) (v).(N{b:=(x).Ax x a}) z" 
@@ -6326,7 +6326,7 @@
   finally show "(OrL (u).M (v).N z){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (OrL (u).M (v).N z)[b\<turnstile>c>a]" using fs by simp
 next
   case (ImpR z c M d b a x)
-  have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "z\<sharp>d" "c\<sharp>d" by fact
+  have fs: "z\<sharp>b" "z\<sharp>a" "z\<sharp>x" "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "z\<sharp>d" "c\<sharp>d" by fact+
   have ih: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   show "(ImpR (z).<c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (ImpR (z).<c>.M d)[b\<turnstile>c>a]"
   proof(cases "b=d")
@@ -6360,7 +6360,7 @@
   qed
 next
   case (ImpL c M u N v b a x)
-  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "c\<sharp>N" "c\<sharp>v" "u\<sharp>M" "u\<sharp>v" by fact
+  have fs: "c\<sharp>b" "c\<sharp>a" "c\<sharp>x" "u\<sharp>b" "u\<sharp>a" "u\<sharp>x" "c\<sharp>N" "c\<sharp>v" "u\<sharp>M" "u\<sharp>v" by fact+
   have ih1: "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]" by fact
   have ih2: "N{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* N[b\<turnstile>c>a]" by fact
   have "(ImpL <c>.M (u).N v){b:=(x).Ax x a} = ImpL <c>.(M{b:=(x).Ax x a}) (u).(N{b:=(x).Ax x a}) v" 
@@ -7124,7 +7124,7 @@
 using a
 proof(nominal_induct M avoiding: x a P b y Q rule: trm.induct)
   case (Ax z c)
-  have fs: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" by fact
+  have fs: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" by fact+
   { assume asm: "z=x \<and> c=b"
     have "(Ax x b){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (x).Ax x b){b:=(y).Q}" using fs by simp
     also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q"
@@ -10052,7 +10052,7 @@
   proof (induct a rule: SNa.induct)
     case (SNaI x)
     note SNa' = this
-    have "SNa b" .
+    have "SNa b" by fact
     thus ?case
     proof (induct b rule: SNa.induct)
       case (SNaI y)
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -168,7 +168,7 @@
 using assms
 proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
   case (Lam y t x u)
-  have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact
+  have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+
   moreover have "x\<sharp> Lam [y].t" by fact 
   ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm)
   moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact
@@ -244,7 +244,7 @@
   ultimately show ?case by auto  
 next
   case (Lam n t x u \<theta>)
-  have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact
+  have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+
   have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact
   have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto
   then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto
@@ -436,7 +436,7 @@
   using assms 
 proof (induct arbitrary: b)
   case (QAN_Reduce x t a b)
-  have h:"x \<leadsto> t" "t \<Down> a" by fact
+  have h:"x \<leadsto> t" "t \<Down> a" by fact+
   have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact
   have "x \<Down> b" by fact
   then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto
@@ -519,14 +519,14 @@
   case (QAP_Var \<Gamma> x T u T')
   have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
   then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
-  moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact
+  moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+
   ultimately show "T=T'" using type_unicity_in_context by auto
 next
   case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u T\<^isub>2')
-  have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
+  have ih: "\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
   have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact
   then obtain r t T\<^isub>1' where "u = App r t"  "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
-  then have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
+  with ih have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
   then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto
 qed (auto)
 
@@ -559,7 +559,7 @@
   case (QAT_Arrow  x \<Gamma> s t T\<^isub>1 T\<^isub>2 u)
   have ih:"(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2 
                                    \<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by fact
-  have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact 
+  have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+
   have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
   then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using fs 
     by (simp add: Q_Arrow_strong_inversion)
@@ -592,7 +592,7 @@
   and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts)
  case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
-  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact
+  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact+
   have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact
   have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
   have "valid \<Gamma>'" by fact
@@ -640,8 +640,8 @@
 next
   case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
   have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" 
-  and  "\<Gamma> \<subseteq> \<Gamma>'" 
-  and  "valid \<Gamma>'" by fact
+  and "\<Gamma> \<subseteq> \<Gamma>'" 
+  and "valid \<Gamma>'" by fact+
   then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by simp
 qed (auto)
 
@@ -797,7 +797,7 @@
     moreover
     { 
       assume "(y,U) \<in> set [(x,T)]"
-      then have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto 
+      with h2 have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
     }
     moreover
     {
@@ -821,7 +821,7 @@
 using h1 h2 h3
 proof (nominal_induct \<Gamma> t T avoiding: \<Gamma>' \<theta> \<theta>'  rule: typing.strong_induct)
   case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
-  have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact
+  have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+
   have h:"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
   have ih:"\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   {
@@ -848,14 +848,14 @@
 proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct)
   case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>')
   have "\<Gamma> \<turnstile> t : T" 
-  and  "valid \<Gamma>'" by fact
+  and  "valid \<Gamma>'" by fact+
   moreover 
   have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
   ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast
 next
   case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>')
   have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
-  and "valid \<Gamma>'" by fact
+  and "valid \<Gamma>'" by fact+
   moreover 
   have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact
   ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast
@@ -864,7 +864,7 @@
   have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact
   have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact
   have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
-  and  v: "valid \<Gamma>'" by fact
+  and  v: "valid \<Gamma>'" by fact+
   then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto
   then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto
   moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto
@@ -872,9 +872,9 @@
 next
   case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   have fs:"x\<sharp>\<Gamma>" by fact
-  have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact 
+  have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
   have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
-  and  h3: "valid \<Gamma>'" by fact
+  and  h3: "valid \<Gamma>'" by fact+
   have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   {
     fix \<Gamma>'' s' t'
@@ -888,7 +888,7 @@
     ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
       using logical_weak_head_closure by auto
   }
-  moreover have "valid \<Gamma>'" using h2 by auto
+  moreover have "valid \<Gamma>'" using h3 by auto
   ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^isub>2> is Lam [x].\<theta>'<t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
   then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs2 by auto
 next
@@ -897,9 +897,9 @@
 next
   case (Q_Beta x \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
-  and  h': "valid \<Gamma>'" by fact
+  and  h': "valid \<Gamma>'" by fact+
   have fs: "x\<sharp>\<Gamma>" by fact
-  have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact 
+  have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
   have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" by fact
   have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^isub>2" by fact
   have "\<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" using ih1 h' h by auto
@@ -914,8 +914,8 @@
 next
   case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
-  and  h2': "valid \<Gamma>'" by fact
-  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
+  and  h2': "valid \<Gamma>'" by fact+
+  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+
   have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> 
                           \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^isub>2" by fact
    {
@@ -930,7 +930,7 @@
     then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta><s>) s'  is App ((x,t')#\<theta>'<t>) t' : T\<^isub>2" by auto
     then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^isub>2" using fs fresh_psubst_simp by auto
   }
-  moreover have "valid \<Gamma>'" using h2 by auto
+  moreover have "valid \<Gamma>'" using h2' by auto
   ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
 next
   case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>')  
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -599,7 +599,7 @@
       hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
       hence T_inst: "T = Top" by (simp add: S_TopE)
       have "\<turnstile> \<Gamma> ok" 
-	and "S closed_in \<Gamma>" by fact
+	and "S closed_in \<Gamma>" by fact+
       hence "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.S_Top)
       thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
     next
@@ -724,13 +724,13 @@
   { --{* The transitivity proof is now by the auxiliary lemma. *}
     case 1 
     have  "\<Gamma> \<turnstile> S <: Q" 
-      and "\<Gamma> \<turnstile> Q <: T" by fact
+      and "\<Gamma> \<turnstile> Q <: T" by fact+
     thus "\<Gamma> \<turnstile> S <: T" by (rule transitivity_aux) 
   next 
     --{* The narrowing proof proceeds by an induction over @{term "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N"}. *}
     case 2
     have  "(\<Delta>@[(X,Q)]@\<Gamma>) \<turnstile> M <: N" --{* left-hand derivation *}
-      and "\<Gamma> \<turnstile> P<:Q" by fact --{* right-hand derivation *}
+      and "\<Gamma> \<turnstile> P<:Q" by fact+ --{* right-hand derivation *}
     thus "(\<Delta>@[(X,P)]@\<Gamma>) \<turnstile> M <: N" 
     proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(X,Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of.strong_induct) 
       case (S_Top _ S \<Delta> \<Gamma> X)
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -64,7 +64,7 @@
   case (Lam y e1)
   hence ih: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" by simp
   moreover
-  have vc: "y\<sharp>x" "y\<sharp>e'" by fact (* usual variable convention *)
+  have vc: "y\<sharp>x" "y\<sharp>e'" by fact+ (* usual variable convention *)
   ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
 next    
   case (App e1 e2)
@@ -74,4 +74,3 @@
 qed
 
 end
-
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -374,7 +374,7 @@
   proof (induct a rule: acc.induct)
     case (accI x)
     note accI' = accI
-    have "acc r b" .
+    have "acc r b" by fact
     thus ?case
     proof (induct b rule: acc.induct)
       case (accI y)
@@ -501,7 +501,7 @@
   case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) --"lambda case"
   have ih: "\<And>\<theta>. \<theta> closes ((a,\<sigma>)#\<Gamma>) \<Longrightarrow> \<theta><t> \<in> RED \<tau>" by fact
   have \<theta>_cond: "\<theta> closes \<Gamma>" by fact
-  have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact
+  have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact+
   from ih have "\<forall>s\<in>RED \<sigma>. ((a,s)#\<theta>)<t> \<in> RED \<tau>" 
     using fresh \<theta>_cond fresh_context by simp
   then have "\<forall>s\<in>RED \<sigma>. \<theta><t>[a::=s] \<in> RED \<tau>" 
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -327,7 +327,7 @@
                   and "(x\<^isub>1, Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> e\<^isub>1 : T" 
                   and "(x\<^isub>2, Data \<sigma>\<^isub>2)#\<Gamma> \<turnstile> e\<^isub>2 : T"
 proof -
-  have f:"x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact
+  have f:"x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact+
   have "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" by fact
   then obtain \<sigma>\<^isub>1 \<sigma>\<^isub>2 x\<^isub>1' x\<^isub>2' e\<^isub>1' e\<^isub>2' where 
     h:"\<Gamma> \<turnstile> e : Data (DSum \<sigma>\<^isub>1 \<sigma>\<^isub>2)" and 
@@ -382,8 +382,8 @@
   then have ih\<^isub>1: "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2) \<Longrightarrow> (x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>1 : T" 
        and  ih\<^isub>2: "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2) \<Longrightarrow> (x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>2 : T" 
        and  ih\<^isub>3: "\<Gamma>\<^isub>2 \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2)" by auto 
-  have fs\<^isub>1: "x\<^isub>1\<sharp>\<Gamma>\<^isub>2" "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>e\<^isub>2" "x\<^isub>1\<sharp>x\<^isub>2" by fact
-  have fs\<^isub>2: "x\<^isub>2\<sharp>\<Gamma>\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>e\<^isub>1" "x\<^isub>2\<sharp>x\<^isub>1" by fact
+  have fs\<^isub>1: "x\<^isub>1\<sharp>\<Gamma>\<^isub>2" "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>e\<^isub>2" "x\<^isub>1\<sharp>x\<^isub>2" by fact+
+  have fs\<^isub>2: "x\<^isub>2\<sharp>\<Gamma>\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>e\<^isub>1" "x\<^isub>2\<sharp>x\<^isub>1" by fact+
   have "valid \<Gamma>\<^isub>2" by fact
   then have "valid ((x\<^isub>1,Data S\<^isub>1)#\<Gamma>\<^isub>2)" and "valid ((x\<^isub>2,Data S\<^isub>2)#\<Gamma>\<^isub>2)" using fs\<^isub>1 fs\<^isub>2 by auto
   then have "(x\<^isub>1, Data S\<^isub>1)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>1 : T" and "(x\<^isub>2, Data S\<^isub>2)#\<Gamma>\<^isub>2 \<turnstile> e\<^isub>2 : T" using ih\<^isub>1 ih\<^isub>2 by simp_all
@@ -439,7 +439,7 @@
   qed
 next
   case (Lam y t \<Gamma> e' x T)
-  have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'"  by fact
+  have vc: "y\<sharp>\<Gamma>" "y\<sharp>x" "y\<sharp>e'"  by fact+
   have pr1: "\<Gamma> \<turnstile> e' : T'" by fact
   have pr2: "(x,T')#\<Gamma> \<turnstile> Lam [y].t : T" by fact
   then obtain T\<^isub>1 T\<^isub>2 where pr2': "(y,T\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t : T\<^isub>2" and eq: "T = T\<^isub>1\<rightarrow>T\<^isub>2" 
@@ -455,7 +455,7 @@
 next
   case (Case t\<^isub>1 x\<^isub>1 t\<^isub>2 x\<^isub>2 t3 \<Gamma> e' x T)
   have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>1\<sharp>e'" "x\<^isub>1\<sharp>x""x\<^isub>1\<sharp>t\<^isub>1" "x\<^isub>1\<sharp>t3" "x\<^isub>2\<sharp>\<Gamma>" 
-           "x\<^isub>2\<sharp>e'" "x\<^isub>2\<sharp>x"  "x\<^isub>2\<sharp>t\<^isub>1" "x\<^isub>2\<sharp>t\<^isub>2" "x\<^isub>2\<noteq>x\<^isub>1" by fact
+           "x\<^isub>2\<sharp>e'" "x\<^isub>2\<sharp>x"  "x\<^isub>2\<sharp>t\<^isub>1" "x\<^isub>2\<sharp>t\<^isub>2" "x\<^isub>2\<noteq>x\<^isub>1" by fact+
   have as1: "\<Gamma> \<turnstile> e' : T'" by fact
   have as2: "(x,T')#\<Gamma> \<turnstile> Case t\<^isub>1 of inl x\<^isub>1 \<rightarrow> t\<^isub>2 | inr x\<^isub>2 \<rightarrow> t3 : T" by fact
   then obtain S\<^isub>1 S\<^isub>2 where 
@@ -463,10 +463,10 @@
     h2:"(x\<^isub>1,Data S\<^isub>1)#(x,T')#\<Gamma> \<turnstile> t\<^isub>2 : T" and
     h3:"(x\<^isub>2,Data S\<^isub>2)#(x,T')#\<Gamma> \<turnstile> t3 : T"
     using vc by (auto simp add: fresh_list_cons)
-  have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> t\<^isub>1 : T; \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1[x::=e'] : T" 
+  have ih1: "\<lbrakk>(x,T')#\<Gamma> \<turnstile> t\<^isub>1 : Data (DSum S\<^isub>1 S\<^isub>2); \<Gamma> \<turnstile> e' : T'\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1[x::=e'] : Data (DSum S\<^isub>1 S\<^isub>2)"
   and  ih2: "\<lbrakk>(x,T')#(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2:T; (x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> e':T'\<rbrakk> \<Longrightarrow> (x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2[x::=e']:T" 
   and  ih3: "\<lbrakk>(x,T')#(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3:T; (x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> e':T'\<rbrakk> \<Longrightarrow> (x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3[x::=e']:T"
-    by fact
+    by fact+
   from h2 have h2': "(x,T')#(x\<^isub>1,Data S\<^isub>1)#\<Gamma> \<turnstile> t\<^isub>2 : T" by (rule context_exchange)
   from h3 have h3': "(x,T')#(x\<^isub>2,Data S\<^isub>2)#\<Gamma> \<turnstile> t3 : T" by (rule context_exchange)
   have "\<Gamma> \<turnstile> t\<^isub>1[x::=e'] : Data (DSum S\<^isub>1 S\<^isub>2)" using h1 ih1 as1 by simp
@@ -663,7 +663,7 @@
   thus "\<Gamma> \<turnstile> e' : T" using ih3 by simp
 next
   case (b_CaseL x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' \<Gamma>)
-  have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact
+  have vc: "x\<^isub>1\<sharp>\<Gamma>" "x\<^isub>2\<sharp>\<Gamma>" by fact+
   have "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T" by fact 
   then obtain S\<^isub>1 S\<^isub>2 e\<^isub>1' e\<^isub>2' where 
     a1: "\<Gamma> \<turnstile> e : Data (DSum S\<^isub>1 S\<^isub>2)" and 
@@ -694,7 +694,7 @@
   have ih2:"\<And>t. e\<^isub>2 \<Down> t \<Longrightarrow> e\<^isub>2' = t" by fact
   have ih3: "\<And>t. e\<^isub>1'[x::=e\<^isub>2'] \<Down> t \<Longrightarrow> e' = t" by fact
   have app: "App e\<^isub>1 e\<^isub>2 \<Down> t\<^isub>2" by fact
-  have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" by fact
+  have vc: "x\<sharp>e\<^isub>1" "x\<sharp>e\<^isub>2" by fact+
   then have "x \<sharp> App e\<^isub>1 e\<^isub>2" by auto
   then have vc': "x\<sharp>t\<^isub>2" using fresh_preserved app by blast
   from vc vc' obtain f\<^isub>1 f\<^isub>2 where x1: "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" and x2: "e\<^isub>2 \<Down> f\<^isub>2" and x3: "f\<^isub>1[x::=f\<^isub>2] \<Down> t\<^isub>2"
@@ -708,7 +708,7 @@
   thus ?case using ih3 by simp
 next
   case (b_CaseL  x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' t\<^isub>2)
-  have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact 
+  have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact+
   have ih1:"\<And>t. e \<Down> t \<Longrightarrow> InL e' = t" by fact 
   have ih2:"\<And>t. e\<^isub>1[x\<^isub>1::=e'] \<Down> t \<Longrightarrow> e'' = t" by fact
   have ha: "\<not>(\<exists>t. e \<Down> InR t)" using ih1 by force
@@ -720,7 +720,7 @@
   then show "e'' = t\<^isub>2" using ih2 by simp
 next 
   case (b_CaseR x\<^isub>1 e e\<^isub>2 e'' x\<^isub>2 e\<^isub>1 e' t\<^isub>2 )
-  have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact 
+  have fs: "x\<^isub>1\<sharp>e" "x\<^isub>1\<sharp>t\<^isub>2" "x\<^isub>2\<sharp>e" "x\<^isub>2\<sharp>t\<^isub>2" by fact+
   have ih1: "\<And>t. e \<Down> t \<Longrightarrow> InR e' = t" by fact
   have ih2: "\<And>t. e\<^isub>2[x\<^isub>2::=e'] \<Down> t \<Longrightarrow> e'' = t" by fact
   have ha: "\<not>(\<exists>t. e \<Down> InL t)" using ih1 by force
@@ -997,7 +997,7 @@
   have ih:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" by fact
   have as\<^isub>1: "\<theta> Vcloses \<Gamma>" by fact
   have as\<^isub>2: "\<Gamma> \<turnstile> Lam [x].e : T" by fact
-  have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact
+  have fs: "x\<sharp>\<Gamma>" "x\<sharp>\<theta>" by fact+
   from as\<^isub>2 fs obtain T\<^isub>1 T\<^isub>2 
     where "(i)": "(x,T\<^isub>1)#\<Gamma> \<turnstile> e:T\<^isub>2" and "(ii)": "T = T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
   from "(i)" have "(iii)": "valid ((x,T\<^isub>1)#\<Gamma>)" by (simp add: typing_implies_valid)
@@ -1016,7 +1016,7 @@
 next
   case (Case t' n\<^isub>1 t\<^isub>1 n\<^isub>2 t\<^isub>2 \<Gamma> \<theta> T)
   have f: "n\<^isub>1\<sharp>\<Gamma>" "n\<^isub>1\<sharp>\<theta>" "n\<^isub>2\<sharp>\<Gamma>" "n\<^isub>2\<sharp>\<theta>" "n\<^isub>2\<noteq>n\<^isub>1" "n\<^isub>1\<sharp>t'"
-  "n\<^isub>1\<sharp>t\<^isub>2" "n\<^isub>2\<sharp>t'" "n\<^isub>2\<sharp>t\<^isub>1" by fact
+  "n\<^isub>1\<sharp>t\<^isub>2" "n\<^isub>2\<sharp>t'" "n\<^isub>2\<sharp>t\<^isub>1" by fact+
   have h:"\<theta> Vcloses \<Gamma>" by fact
   have th:"\<Gamma> \<turnstile> Case t' of inl n\<^isub>1 \<rightarrow> t\<^isub>1 | inr n\<^isub>2 \<rightarrow> t\<^isub>2 : T" by fact
   then obtain S\<^isub>1 S\<^isub>2 where 
diff -r 4b03e3586f7f -r 31781b2de73d src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Jun 14 23:04:36 2007 +0200
@@ -1715,7 +1715,7 @@
   and     at: "at TYPE('x)"
   shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
 proof -
-  have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+  have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8 [OF at])
   hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis by (simp add: pt2[OF pt])
 qed
@@ -2543,7 +2543,7 @@
 proof -
   have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) 
   have ptc: "pt TYPE('y\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
-  have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb,OF cpa])
+  have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb cpa ptb at])
   have f2: "finite ((supp (pi\<bullet>h))::'y set)"
   proof -
     from f1 have "finite (pi\<bullet>((supp h)::'y set))"
@@ -3077,7 +3077,7 @@
   and     at: "at TYPE('x)"
   shows "pi2\<bullet>(pi1\<bullet>x) = perm_aux (pi2\<bullet>pi1) (pi2\<bullet>x)" 
 proof -
-  have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+  have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8[OF at])
   hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis by (simp add: pt2[OF pt] perm_aux_def)
 qed