diff -r 28e9c770a082 -r 88f831f86b96 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 08 13:08:56 2009 +0100 +++ b/Quot/Examples/FSet.thy Tue Dec 08 13:09:21 2009 +0100 @@ -446,7 +446,7 @@ sorry lemma "(\x. (FUNION x (INSERT e EMPTY))) = (\x. (INSERT e x))" -apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) +(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) sorry end