tuned signature;

--- a/src/HOL/Library/bnf_axiomatization.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -35,9 +35,9 @@
     fun mk_b name user_b =
       (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
       |> Binding.qualify false (Binding.name_of b);
-    val (Tname, lthy) = Typedecl.basic_typedecl true (b, length vars, mx) lthy;
-    val (bd_type_Tname, lthy) =
-      Typedecl.basic_typedecl true (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
+    val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy;
+    val (bd_type_Tname, lthy) = lthy
+      |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn);
     val T = Type (Tname, map TFree vars);
     val bd_type_T = Type (bd_type_Tname, map TFree deads);
     val lives = map TFree (filter_out (member (op =) deads) vars);

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -388,8 +388,7 @@
       (ids,
        case get_type thy prfx s of
          SOME _ => thy
-       | NONE => Typedecl.typedecl_global
-           true (Binding.name s, [], NoSyn) thy |> snd);
+       | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);
 
 
 fun term_of_expr thy prfx types pfuns =

--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -198,9 +198,8 @@
       val final_fqn = Sign.full_name thy binding
       val tyargs =
         List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int)
-      val thy' =
-        Typedecl.typedecl_global true (mk_binding config type_name, tyargs, NoSyn) thy
-        |> snd
+      val (_, thy') =
+        Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy
       val typ_map_entry = (thf_type, (final_fqn, arity))
       val ty_map' = typ_map_entry :: ty_map
     in (ty_map', thy') end

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -1923,7 +1923,8 @@
       ||>> variant_tfrees fp_b_names;
 
     fun add_fake_type spec =
-      Typedecl.basic_typedecl true (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
+      Typedecl.basic_typedecl {final = true}
+        (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
 
     val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy;
 

--- a/src/HOL/Tools/typedef.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -194,7 +194,7 @@
 
     val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args;
     val (newT, typedecl_lthy) = lthy
-      |> Typedecl.typedecl false (name, args, mx)
+      |> Typedecl.typedecl {final = false} (name, args, mx)
       ||> Variable.declare_term set;
 
     val Type (full_name, _) = newT;

--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 23 09:36:18 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 23 09:50:38 2015 +0200
@@ -22,7 +22,8 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
-      >> (fn ((args, a), mx) => Typedecl.typedecl true (a, map (rpair dummyS) args, mx) #> snd));
+      >> (fn ((args, a), mx) =>
+          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"

--- 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;