src/Pure/Isar/constdefs.ML

     val atts = map (prep_att thy) raw_atts;
 
     val thy' =
       thy
       |> Theory.add_consts_i [(c, T, mx)]
-      |> PureThy.add_defs_i false [((name, def), atts)] |> #1;
+      |> PureThy.add_defs_i false [((name, def), atts)]
+      |> snd;
   in ((c, T), thy') end;
 
 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy =
   let
     val structs = #1 (fold_map prep_vars raw_structs (ProofContext.init thy));