src/HOLCF/Tools/Domain/domain_syntax.ML
changeset 35446 8cb42aa19358
parent 35432 b719dad322fa
child 35448 f5461b02d754
     1.1 --- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Sat Feb 27 14:04:46 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Sat Feb 27 15:32:42 2010 -0800
     1.3 @@ -64,15 +64,10 @@
     1.4            | esc []      = []
     1.5        in implode o esc o Symbol.explode end;
     1.6  
     1.7 -      fun dis_name_ con =
     1.8 -          Binding.name ("is_" ^ strip_esc (Binding.name_of con));
     1.9        fun mat_name_ con =
    1.10            Binding.name ("match_" ^ strip_esc (Binding.name_of con));
    1.11        fun pat_name_ con =
    1.12            Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
    1.13 -      fun dis (con,args,mx) =
    1.14 -          (dis_name_ con, dtype->>trT,
    1.15 -           Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
    1.16        (* strictly speaking, these constants have one argument,
    1.17         but the mixfix (without arguments) is introduced only
    1.18             to generate parse rules for non-alphanumeric names*)
    1.19 @@ -95,7 +90,6 @@
    1.20               mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
    1.21             Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
    1.22      in
    1.23 -    val consts_dis = map dis cons';
    1.24      val consts_mat = map mat cons';
    1.25      val consts_pat = map pat cons';
    1.26      end;
    1.27 @@ -165,7 +159,7 @@
    1.28          if definitional then [] else [const_rep, const_abs, const_copy];
    1.29  
    1.30    in (optional_consts @ [const_when] @ 
    1.31 -      consts_dis @ consts_mat @ consts_pat @
    1.32 +      consts_mat @ consts_pat @
    1.33        [const_take, const_finite],
    1.34        (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
    1.35    end; (* let *)