# HG changeset patch
# User blanchet
# Date 1410294823 -7200
# Node ID eb93bc67d36135c7214bf922befe436162c787be
# Parent  87b59745dd6dd568d370a6ebe6599d40b9ddaf25
avoid exception

diff -r 87b59745dd6d -r eb93bc67d361 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 22:28:49 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 09 22:33:43 2014 +0200
@@ -291,7 +291,7 @@
     Long_Name.map_base_name (prefix isN) (name_of_disc t')
   | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
     Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
-  | t' => name_of_const "discriminator" domain_type t');
+  | t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
 
 val base_name_of_ctr = Long_Name.base_name o name_of_ctr;