src/HOL/Tools/typedef.ML

             Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
           Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
       in
         lthy2
-        |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
+        |> Local_Theory.declaration {syntax = false, pervasive = true}
+          (fn phi => put_info full_tname (transform_info phi info))
         |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
         |> pair (full_tname, info)
       end;
 
   in ((goal, goal_pat, typedef_result), alias_lthy) end