src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
changeset 58182 82478e6c60cb
parent 58112 8081087096ad
child 58274 4a84e94e58a2
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Thu Sep 04 11:20:59 2014 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  signature OLD_DATATYPE_REALIZER =
     1.5  sig
     1.6    val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
     1.7 -  val setup: theory -> theory
     1.8  end;
     1.9  
    1.10  structure Old_Datatype_Realizer : OLD_DATATYPE_REALIZER =
    1.11 @@ -158,9 +157,7 @@
    1.12  
    1.13    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    1.14  
    1.15 -
    1.16 -fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info)
    1.17 -    thy =
    1.18 +fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
    1.19    let
    1.20      val ctxt = Proof_Context.init_global thy;
    1.21      val cert = cterm_of thy;
    1.22 @@ -241,6 +238,6 @@
    1.23        |> fold_rev make_casedists infos
    1.24      end;
    1.25  
    1.26 -val setup = Old_Datatype_Data.interpretation add_dt_realizers;
    1.27 +val _ = Theory.setup (Old_Datatype_Data.interpretation add_dt_realizers);
    1.28  
    1.29  end;