diff -r 77eccce38a17 -r f4e241829b80 Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 19:11:51 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 20:01:18 2010 +0200
@@ -261,8 +261,6 @@
 syntax (HTML output)
 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
 
-ML {* Syntax.check_term @{context} (Const ("List.append", dummyT) $ @{term "[3::nat,4]"}) *}
-
 parse_translation (advanced) {*
 let
   val femptyC = Syntax.const @{const_name fempty};