src/HOL/Tools/datatype_realizer.ML
changeset 58277 0dcd3a623a6e
parent 58275 280ede57a6a9
child 58354 04ac60da613e
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -7,14 +7,14 @@
     1.4  
     1.5  signature DATATYPE_REALIZER =
     1.6  sig
     1.7 -  val realizer_plugin: string
     1.8 +  val extraction_plugin: string
     1.9    val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
    1.10  end;
    1.11  
    1.12  structure Datatype_Realizer : DATATYPE_REALIZER =
    1.13  struct
    1.14  
    1.15 -val realizer_plugin = "realizer";
    1.16 +val extraction_plugin = "extraction";
    1.17  
    1.18  fun subsets i j =
    1.19    if i <= j then
    1.20 @@ -158,10 +158,7 @@
    1.21            (map Logic.unvarify_global ivs1 @ filter_out is_unit
    1.22                (map (head_of o strip_abs_body) rec_fns)) r);
    1.23  
    1.24 -  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end
    1.25 -  (* Nested new-style datatypes are not supported (unless they are registered via
    1.26 -     "datatype_compat"). *)
    1.27 -  handle Old_Datatype_Aux.Datatype => thy;
    1.28 +  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    1.29  
    1.30  fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
    1.31    let
    1.32 @@ -240,11 +237,11 @@
    1.33        val info :: _ = infos;
    1.34      in
    1.35        thy
    1.36 -      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
    1.37 -      |> fold_rev make_casedists infos
    1.38 +      |> fold_rev (perhaps o try o make_ind info) (subsets 0 (length (#descr info) - 1))
    1.39 +      |> fold_rev (perhaps o try o make_casedists) infos
    1.40      end;
    1.41  
    1.42 -val _ = Theory.setup (BNF_LFP_Compat.interpretation realizer_plugin BNF_LFP_Compat.Unfold_Nesting
    1.43 +val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin BNF_LFP_Compat.Unfold_Nesting
    1.44    add_dt_realizers);
    1.45  
    1.46  end;