--- a/src/Pure/Isar/typedecl.ML Wed Sep 23 09:36:18 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML Wed Sep 23 09:50:38 2015 +0200
@@ -7,9 +7,12 @@
signature TYPEDECL =
sig
val read_constraint: Proof.context -> string option -> sort
- val basic_typedecl: bool -> binding * int * mixfix -> local_theory -> string * local_theory
- val typedecl: bool -> binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
- val typedecl_global: bool -> binding * (string * sort) list * mixfix -> theory -> typ * theory
+ val basic_typedecl: {final: bool} -> binding * int * mixfix ->
+ local_theory -> string * local_theory
+ val typedecl: {final: bool} -> binding * (string * sort) list * mixfix ->
+ local_theory -> typ * local_theory
+ val typedecl_global: {final: bool} -> binding * (string * sort) list * mixfix ->
+ theory -> typ * theory
val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
@@ -62,7 +65,7 @@
Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy
end;
-fun basic_typedecl final (b, n, mx) lthy =
+fun basic_typedecl {final} (b, n, mx) lthy =
lthy
|> basic_decl (fn name =>
Sign.add_type lthy (b, n, NoSyn) #>
@@ -74,18 +77,18 @@
(* type declarations *)
-fun typedecl final (b, raw_args, mx) lthy =
+fun typedecl {final} (b, raw_args, mx) lthy =
let val T = global_type lthy (b, raw_args) in
lthy
- |> basic_typedecl final (b, length raw_args, mx)
+ |> basic_typedecl {final = final} (b, length raw_args, mx)
|> snd
|> Variable.declare_typ T
|> pair T
end;
-fun typedecl_global final decl =
+fun typedecl_global {final} decl =
Named_Target.theory_init
- #> typedecl final decl
+ #> typedecl {final = final} decl
#> Local_Theory.exit_result_global Morphism.typ;