src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57260 8747af0d1012
parent 57200 aab87ffa60cc
child 57629 e88b5f59cade
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 16 17:52:33 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 16 19:18:10 2014 +0200
     1.3 @@ -262,17 +262,16 @@
     1.4  val name_of_ctr = name_of_const "constructor";
     1.5  
     1.6  val notN = "not_";
     1.7 -val eqN = "eq_";
     1.8 -val neqN = "neq_";
     1.9 +val isN = "is_";
    1.10  
    1.11  fun name_of_disc t =
    1.12    (case head_of t of
    1.13      Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
    1.14      Long_Name.map_base_name (prefix notN) (name_of_disc t')
    1.15    | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
    1.16 -    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
    1.17 +    Long_Name.map_base_name (prefix isN) (name_of_disc t')
    1.18    | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
    1.19 -    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
    1.20 +    Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
    1.21    | t' => name_of_const "destructor" t');
    1.22  
    1.23  val base_name_of_ctr = Long_Name.base_name o name_of_ctr;