src/Pure/ML/exn_properties_dummy.ML
changeset 50911 ee7fe4230642
child 60865 4194901fd513
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/exn_properties_dummy.ML	Wed Jan 16 16:26:36 2013 +0100
     1.3 @@ -0,0 +1,20 @@
     1.4 +(*  Title:      Pure/ML/exn_properties_dummy.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Exception properties -- dummy version.
     1.8 +*)
     1.9 +
    1.10 +signature EXN_PROPERTIES =
    1.11 +sig
    1.12 +  val get: exn -> Properties.T
    1.13 +  val update: Properties.entry list -> exn -> exn
    1.14 +end;
    1.15 +
    1.16 +structure Exn_Properties: EXN_PROPERTIES =
    1.17 +struct
    1.18 +
    1.19 +fun get _ = [];
    1.20 +fun update _ exn = exn;
    1.21 +
    1.22 +end;
    1.23 +