src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML

               def
             end
          val new_defs = map new_def assms
          val (definition, thy') = thy
           |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> fold_map Drule.add_axiom (map_index
-              (fn (i, t) => (Binding.name (constname ^ "_def" ^ string_of_int i), t)) new_defs)
+          |> fold_map Specification.axiom (map_index
+              (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
         in
-          (lhs, ((full_constname, definition) :: defs, thy'))
+          (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
         end
       else
         (atom, (defs, thy)))
 
 fun flatten_intros constname intros thy =