# HG changeset patch
# User wenzelm
# Date 1256652151 -3600
# Node ID 9a2911232c1b4753557262e6c49aba4f4053cc0b
# Parent  0496565527bd29b57bd997322798b22eb4b5eebe
comment;

diff -r 0496565527bd -r 9a2911232c1b src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 13:34:37 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 15:02:31 2009 +0100
@@ -90,6 +90,7 @@
 
     fun make_cpo admissible (type_def, below_def, set_def) theory =
       let
+        (* FIXME fold_rule might fold user input inintentionally *)
         val admissible' = fold_rule (the_list set_def) admissible;
         val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
         val theory' = theory
@@ -112,6 +113,7 @@
 
     fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
       let
+        (* FIXME fold_rule might fold user input inintentionally *)
         val UU_mem' = fold_rule (the_list set_def) UU_mem;
         val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
         val theory' = theory