src/Pure/Isar/typedecl.ML
changeset 61261 ddb2da7cb2e4
parent 61259 6dc3d5d50e57
child 69732 49d25343d3d4
     1.1 --- a/src/Pure/Isar/typedecl.ML	Thu Sep 24 13:33:42 2015 +0200
     1.2 +++ b/src/Pure/Isar/typedecl.ML	Thu Sep 24 23:33:29 2015 +0200
     1.3 @@ -62,7 +62,8 @@
     1.4      val c = Local_Theory.full_name lthy b;
     1.5      val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
     1.6    in
     1.7 -    Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy
     1.8 +    Local_Theory.background_theory
     1.9 +      (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy
    1.10    end;
    1.11  
    1.12  fun basic_typedecl {final} (b, n, mx) lthy =