src/HOL/Tools/datatype_realizer.ML
changeset 58354 04ac60da613e
parent 58277 0dcd3a623a6e
child 58659 6c9821c32dd5
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Sep 17 08:23:53 2014 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4    else
     1.5      let
     1.6        val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
     1.7 -      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
     1.8 +      val infos = map (BNF_LFP_Compat.the_info thy []) names;
     1.9        val info :: _ = infos;
    1.10      in
    1.11        thy
    1.12 @@ -241,7 +241,6 @@
    1.13        |> fold_rev (perhaps o try o make_casedists) infos
    1.14      end;
    1.15  
    1.16 -val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin BNF_LFP_Compat.Unfold_Nesting
    1.17 -  add_dt_realizers);
    1.18 +val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
    1.19  
    1.20  end;