# HG changeset patch
# User haftmann
# Date 1496671185 -7200
# Node ID 39d9a59d8d94563b71def3ba5c133f64a55fca9b
# Parent  70643edecb7af261a23a82691080f90516280bd2
tuned

diff -r 70643edecb7a -r 39d9a59d8d94 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jun 05 15:59:45 2017 +0200
@@ -17,8 +17,8 @@
 \<close>
 
 declare [[code drop:
-  Sup_pred_inst.Sup_pred
-  Inf_pred_inst.Inf_pred
+  "Inf :: _ Predicate.pred set \<Rightarrow> _"
+  "Sup :: _ Predicate.pred set \<Rightarrow> _"
   pred_of_set
   Wellfounded.acc
   Cardinality.card'
@@ -27,25 +27,25 @@
   Cardinality.eq_set
   Gcd_fin
   Lcm_fin
+  Euclidean_Algorithm.Gcd
+  Euclidean_Algorithm.Lcm
   "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:
-  '"List.set" is not a constructor, on left hand side of equation: ...',
-  the code equation in question has to be either deleted (like many others in this file) 
-  or implemented for RBT trees.
-*)
-
+text \<open>
+  If code generation fails with a message like
+  @{text \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>},
+  feel free to add an RBT implementation for the corrsponding operation
+  of delete that code equation (see above).
+\<close>
+ 
 export_code _ checking SML OCaml? Haskell? Scala
 
 end