--- a/src/Pure/Isar/typedecl.ML Thu Sep 24 13:33:42 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML Thu Sep 24 23:33:29 2015 +0200
@@ -62,7 +62,8 @@
val c = Local_Theory.full_name lthy b;
val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
in
- Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy
+ Local_Theory.background_theory
+ (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy
end;
fun basic_typedecl {final} (b, n, mx) lthy =