diff -r ae0bbc8e45ad -r 340db65fd2c1 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jan 04 21:28:29 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jan 04 21:28:29 2017 +0100
@@ -20,64 +20,31 @@
 in fold Code.del_eqns consts thy end
 \<close> \<comment> \<open>drop technical stuff from \<open>Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
 
-(* 
-   The following code equations have to be deleted because they use 
-   lists to implement sets in the code generetor. 
-*)
-
-lemma [code, code del]:
-  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
-
-lemma [code, code del]:
-  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
-
-lemma [code, code del]:
-  "pred_of_set = pred_of_set" ..
-
-lemma [code, code del]:
-  "Wellfounded.acc = Wellfounded.acc" ..
-
-lemma [code, code del]:
-  "Cardinality.card' = Cardinality.card'" ..
-
-lemma [code, code del]:
-  "Cardinality.finite' = Cardinality.finite'" ..
-
-lemma [code, code del]:
-  "Cardinality.subset' = Cardinality.subset'" ..
-
-lemma [code, code del]:
-  "Cardinality.eq_set = Cardinality.eq_set" ..
+text \<open>
+  The following code equations have to be deleted because they use 
+  lists to implement sets in the code generetor. 
+\<close>
 
-lemma [code, code del]:
-  "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
-
-lemma [code, code del]:
-  "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
-
-lemma [code, code del]:
-  "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
-
-lemma [code, code del]:
-  "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
-
-lemma [code, code del]:
-  "(Gcd :: _ poly set \<Rightarrow> _) = Gcd" ..
-
-lemma [code, code del]:
-  "(Lcm :: _ poly set \<Rightarrow> _) = Lcm" ..
-
-lemma [code, code del]:
-  "Gcd_eucl = Gcd_eucl" ..
-
-lemma [code, code del]:
-  "Lcm_eucl = Lcm_eucl" ..
-
-lemma [code, code del]:
-  "permutations_of_set = permutations_of_set" ..
-
-lemma [code, code del]:
-  "permutations_of_multiset = permutations_of_multiset" ..
+declare [[code drop:
+  Sup_pred_inst.Sup_pred
+  Inf_pred_inst.Inf_pred
+  pred_of_set
+  Wellfounded.acc
+  Cardinality.card'
+  Cardinality.finite'
+  Cardinality.subset'
+  Cardinality.eq_set
+  "Gcd :: nat set \<Rightarrow> nat"
+  "Lcm :: nat set \<Rightarrow> nat"
+  "Gcd :: int set \<Rightarrow> int"
+  "Lcm :: int set \<Rightarrow> int"
+  "Gcd :: _ poly set \<Rightarrow> _"
+  "Lcm :: _ poly set \<Rightarrow> _"
+  Euclidean_Algorithm.Gcd
+  Euclidean_Algorithm.Lcm
+  permutations_of_set
+  permutations_of_multiset
+]]
 
 (*
   If the code generation ends with an exception with the following message: