add_dummies no longer uses transform_error but handles specific
authorberghofe
Tue Jun 08 19:25:27 2004 +0200 (2004-06-08)
changeset 1488899ac3eb0f84e
parent 14887 4938ce4ef295
child 14889 d7711d6b9014
add_dummies no longer uses transform_error but handles specific
exception Datatype_Empty instead.
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 08 19:23:53 2004 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 08 19:25:27 2004 +0200
     1.3 @@ -234,22 +234,18 @@
     1.4      end
     1.5    end;
     1.6  
     1.7 -val nonempty_msg = explode "Nonemptiness check failed for datatype ";
     1.8 -
     1.9  fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
    1.10    if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
    1.11    else x;
    1.12  
    1.13  fun add_dummies f dts used thy =
    1.14 -  apsnd (pair (map fst dts)) (transform_error (f (map snd dts)) thy)
    1.15 -  handle ERROR_MESSAGE msg => if nonempty_msg prefix explode msg then
    1.16 +  apsnd (pair (map fst dts)) (f (map snd dts) thy)
    1.17 +  handle DatatypeAux.Datatype_Empty name' =>
    1.18        let
    1.19 -        val name = Sign.base_name
    1.20 -          (implode (drop (length nonempty_msg, explode msg)));
    1.21 +        val name = Sign.base_name name';
    1.22          val dname = variant used "Dummy"
    1.23        in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy
    1.24 -      end
    1.25 -    else error msg;
    1.26 +      end;
    1.27  
    1.28  fun mk_realizer thy vs params ((rule, rrule), rt) =
    1.29    let
    1.30 @@ -312,7 +308,7 @@
    1.31  
    1.32      val (thy2, (dummies, dt_info)) = thy1 |>
    1.33        (if null dts then rpair ([], None) else
    1.34 -        apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false
    1.35 +        apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false false
    1.36            (map #2 dts)) (map (pair false) dts) []) |>>
    1.37        Extraction.add_typeof_eqns_i ty_eqs |>>
    1.38        Extraction.add_realizes_eqns_i rlz_eqs;