avoid exception
authorblanchet
Tue Sep 09 22:33:43 2014 +0200 (2014-09-09)
changeset 58289eb93bc67d361
parent 58288 87b59745dd6d
child 58290 14e186d2dd3a
avoid exception
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 22:28:49 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 22:33:43 2014 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4      Long_Name.map_base_name (prefix isN) (name_of_disc t')
     1.5    | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
     1.6      Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
     1.7 -  | t' => name_of_const "discriminator" domain_type t');
     1.8 +  | t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
     1.9  
    1.10  val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
    1.11