src/HOLCF/Tools/pcpodef.ML
changeset 33226 9a2911232c1b
parent 31740 002da20f442e
child 33553 35f2b30593a8
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 13:34:37 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 15:02:31 2009 +0100
     1.3 @@ -90,6 +90,7 @@
     1.4  
     1.5      fun make_cpo admissible (type_def, below_def, set_def) theory =
     1.6        let
     1.7 +        (* FIXME fold_rule might fold user input inintentionally *)
     1.8          val admissible' = fold_rule (the_list set_def) admissible;
     1.9          val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
    1.10          val theory' = theory
    1.11 @@ -112,6 +113,7 @@
    1.12  
    1.13      fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
    1.14        let
    1.15 +        (* FIXME fold_rule might fold user input inintentionally *)
    1.16          val UU_mem' = fold_rule (the_list set_def) UU_mem;
    1.17          val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
    1.18          val theory' = theory