src/HOL/Nominal/nominal_datatype.ML
changeset 32960 69916a850301
parent 32957 675c0c7e6a37
child 33035 15eab423e573
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1107,7 +1107,7 @@
     1.4  
     1.5      val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
     1.6  
     1.7 -	(* Function to add both the simp and eqvt attributes *)
     1.8 +        (* Function to add both the simp and eqvt attributes *)
     1.9          (* These two attributes are duplicated on all the types in the mutual nominal datatypes *)
    1.10  
    1.11      val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];