src/HOL/Tools/datatype_realizer.ML
changeset 58659 6c9821c32dd5
parent 58354 04ac60da613e
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 13 17:04:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 13 18:45:48 2014 +0200
     1.3 @@ -7,15 +7,12 @@
     1.4  
     1.5  signature DATATYPE_REALIZER =
     1.6  sig
     1.7 -  val extraction_plugin: string
     1.8    val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
     1.9  end;
    1.10  
    1.11  structure Datatype_Realizer : DATATYPE_REALIZER =
    1.12  struct
    1.13  
    1.14 -val extraction_plugin = "extraction";
    1.15 -
    1.16  fun subsets i j =
    1.17    if i <= j then
    1.18      let val is = subsets (i+1) j
    1.19 @@ -241,6 +238,6 @@
    1.20        |> fold_rev (perhaps o try o make_casedists) infos
    1.21      end;
    1.22  
    1.23 -val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
    1.24 +val _ = Theory.setup (BNF_LFP_Compat.interpretation @{plugin extraction} [] add_dt_realizers);
    1.25  
    1.26  end;