equal
deleted
inserted
replaced
60 fun final_type (b, n) lthy = |
60 fun final_type (b, n) lthy = |
61 let |
61 let |
62 val c = Local_Theory.full_name lthy b; |
62 val c = Local_Theory.full_name lthy b; |
63 val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); |
63 val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); |
64 in |
64 in |
65 Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy |
65 Local_Theory.background_theory |
|
66 (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy |
66 end; |
67 end; |
67 |
68 |
68 fun basic_typedecl {final} (b, n, mx) lthy = |
69 fun basic_typedecl {final} (b, n, mx) lthy = |
69 lthy |
70 lthy |
70 |> basic_decl (fn name => |
71 |> basic_decl (fn name => |