src/HOL/Tools/inductive_realizer.ML
changeset 45701 615da8b8d758
parent 44241 7943b69f0188
child 45839 43a5b86bc102
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Nov 30 21:14:01 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Nov 30 23:30:08 2011 +0100
     1.3 @@ -305,15 +305,15 @@
     1.4  
     1.5      val ((dummies, some_dt_names), thy2) =
     1.6        thy1
     1.7 -      |> add_dummies (Datatype.add_datatype
     1.8 -           { strict = false, quiet = false } (map (Binding.name_of o #2) dts))
     1.9 -           (map (pair false) dts) []
    1.10 +      |> add_dummies (Datatype.add_datatype {strict = false, quiet = false})
    1.11 +        (map (pair false) dts) []
    1.12        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.13        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    1.14      val dt_names = these some_dt_names;
    1.15      val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
    1.16 -    val rec_thms = if null dt_names then []
    1.17 -      else (#rec_rewrites o Datatype.the_info thy2) (hd dt_names);
    1.18 +    val rec_thms =
    1.19 +      if null dt_names then []
    1.20 +      else #rec_rewrites (Datatype.the_info thy2 (hd dt_names));
    1.21      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
    1.22        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
    1.23      val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>