1.1 --- a/etc/isar-keywords-ZF.el	Fri Mar 16 22:31:19 2012 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Fri Mar 16 22:48:38 2012 +0100
     1.3 @@ -61,7 +61,6 @@
     1.4      "exit"
     1.5      "extract"
     1.6      "extract_type"
     1.7 -    "finalconsts"
     1.8      "finally"
     1.9      "find_consts"
    1.10      "find_theorems"
    1.11 @@ -359,7 +358,6 @@
    1.12      "defs"
    1.13      "extract"
    1.14      "extract_type"
    1.15 -    "finalconsts"
    1.16      "hide_class"
    1.17      "hide_const"
    1.18      "hide_fact"

     2.1 --- a/etc/isar-keywords.el	Fri Mar 16 22:31:19 2012 +0100
     2.2 +++ b/etc/isar-keywords.el	Fri Mar 16 22:48:38 2012 +0100
     2.3 @@ -88,7 +88,6 @@
     2.4      "export_code"
     2.5      "extract"
     2.6      "extract_type"
     2.7 -    "finalconsts"
     2.8      "finally"
     2.9      "find_consts"
    2.10      "find_theorems"
    2.11 @@ -478,7 +477,6 @@
    2.12      "equivariance"
    2.13      "extract"
    2.14      "extract_type"
    2.15 -    "finalconsts"
    2.16      "fixrec"
    2.17      "fun"
    2.18      "hide_class"

     3.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Mar 16 22:31:19 2012 +0100
     3.2 +++ b/src/HOL/Tools/choice_specification.ML	Fri Mar 16 22:48:38 2012 +0100
     3.3 @@ -20,6 +20,12 @@
     3.4      fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
     3.5               (map dest_Free (Misc_Legacy.term_frees t)) t
     3.6  
     3.7 +fun add_final overloaded (c, T) thy =
     3.8 +  let
     3.9 +    val ctxt = Syntax.init_pretty_global thy;
    3.10 +    val _ = Theory.check_overloading ctxt overloaded (c, T);
    3.11 +  in Theory.add_deps ctxt "" (c, T) [] thy end;
    3.12 +
    3.13  local
    3.14      fun mk_definitional [] arg = arg
    3.15        | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
    3.16 @@ -58,8 +64,8 @@
    3.17                          val cdefname = if thname = ""
    3.18                                         then Thm.def_name (Long_Name.base_name cname)
    3.19                                         else thname
    3.20 -                        val co = Const(cname_full,ctype)
    3.21 -                        val thy' = Theory.add_finals_i covld [co] thy
    3.22 +                        val thy' = add_final covld (cname_full,ctype) thy
    3.23 +                        val co = Const (cname_full,ctype)
    3.24                          val tm' = case P of
    3.25                                        Abs(_, _, bodt) => subst_bound (co, bodt)
    3.26                                      | _ => P $ co

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 16 22:31:19 2012 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 16 22:48:38 2012 +0100
     4.3 @@ -159,10 +159,6 @@
     4.4  
     4.5  val opt_overloaded = Parse.opt_keyword "overloaded";
     4.6  
     4.7 -val _ =
     4.8 -  Outer_Syntax.command ("finalconsts", Keyword.thy_decl) "declare constants as final"
     4.9 -    (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
    4.10 -
    4.11  val mode_spec =
    4.12    (Parse.$$$ "output" >> K ("", false)) ||
    4.13      Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;

     5.1 --- a/src/Pure/theory.ML	Fri Mar 16 22:31:19 2012 +0100
     5.2 +++ b/src/Pure/theory.ML	Fri Mar 16 22:48:38 2012 +0100
     5.3 @@ -33,9 +33,8 @@
     5.4    val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
     5.5    val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
     5.6    val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
     5.7 -  val add_finals_i: bool -> term list -> theory -> theory
     5.8 -  val add_finals: bool -> string list -> theory -> theory
     5.9    val specify_const: (binding * typ) * mixfix -> theory -> term * theory
    5.10 +  val check_overloading: Proof.context -> bool -> string * typ -> unit
    5.11  end
    5.12  
    5.13  structure Theory: THEORY =
    5.14 @@ -267,28 +266,4 @@
    5.15  
    5.16  end;
    5.17  
    5.18 -
    5.19 -(* add_finals(_i) *)
    5.20 -
    5.21 -local
    5.22 -
    5.23 -fun gen_add_finals prep_term overloaded args thy =
    5.24 -  let
    5.25 -    val ctxt = Syntax.init_pretty_global thy;
    5.26 -    fun const_of (Const const) = const
    5.27 -      | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    5.28 -      | const_of _ = error "Attempt to finalize non-constant term";
    5.29 -    fun specify (c, T) = dependencies ctxt false NONE (c ^ " axiom") (c, T) [];
    5.30 -    val finalize =
    5.31 -      specify o tap (check_overloading ctxt overloaded) o const_of o
    5.32 -        Sign.cert_term thy o prep_term ctxt;
    5.33 -  in thy |> map_defs (fold finalize args) end;
    5.34 -
    5.35 -in
    5.36 -
    5.37 -val add_finals_i = gen_add_finals (K I);
    5.38 -val add_finals = gen_add_finals Syntax.read_term;
    5.39 -
    5.40  end;
    5.41 -
    5.42 -end;