# HG changeset patch # User wenzelm # Date 1442994638 -7200 # Node ID 6dc3d5d50e57c89ee3b7d0b9f364fc3e3c51c5fd # Parent 2be9ea29f9eccae14fc31e6468bd8bf732c515fc tuned signature; diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/HOL/Library/bnf_axiomatization.ML --- 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); diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/HOL/SPARK/Tools/spark_vcs.ML --- 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 = diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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 diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/HOL/Tools/typedef.ML --- 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; diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/Pure/Isar/isar_syn.ML --- 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" diff -r 2be9ea29f9ec -r 6dc3d5d50e57 src/Pure/Isar/typedecl.ML --- 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;