src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57700 a2c4adb839a9
parent 57633 4ff8c090d580
child 57882 38bf4de248a6
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 30 00:50:41 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Jul 30 10:50:28 2014 +0200
     1.3 @@ -255,12 +255,6 @@
     1.4  fun mk_disc_or_sel Ts t =
     1.5    subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
     1.6  
     1.7 -fun name_of_const what t =
     1.8 -  (case head_of t of
     1.9 -    Const (s, _) => s
    1.10 -  | Free (s, _) => s
    1.11 -  | _ => error ("Cannot extract name of " ^ what));
    1.12 -
    1.13  val name_of_ctr = name_of_const "constructor";
    1.14  
    1.15  fun name_of_disc t =