# HG changeset patch
# User wenzelm
# Date 1331934518 -3600
# Node ID 7ca3608146d85c7adf72a71147ba03e84276a847
# Parent  d68798000e467516165139602ee24775acc6f18c
eliminated odd 'finalconsts' / Theory.add_finals;

diff -r d68798000e46 -r 7ca3608146d8 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Mar 16 22:31:19 2012 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Mar 16 22:48:38 2012 +0100
@@ -61,7 +61,6 @@
     "exit"
     "extract"
     "extract_type"
-    "finalconsts"
     "finally"
     "find_consts"
     "find_theorems"
@@ -359,7 +358,6 @@
     "defs"
     "extract"
     "extract_type"
-    "finalconsts"
     "hide_class"
     "hide_const"
     "hide_fact"
diff -r d68798000e46 -r 7ca3608146d8 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Mar 16 22:31:19 2012 +0100
+++ b/etc/isar-keywords.el	Fri Mar 16 22:48:38 2012 +0100
@@ -88,7 +88,6 @@
     "export_code"
     "extract"
     "extract_type"
-    "finalconsts"
     "finally"
     "find_consts"
     "find_theorems"
@@ -478,7 +477,6 @@
     "equivariance"
     "extract"
     "extract_type"
-    "finalconsts"
     "fixrec"
     "fun"
     "hide_class"
diff -r d68798000e46 -r 7ca3608146d8 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Fri Mar 16 22:31:19 2012 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Fri Mar 16 22:48:38 2012 +0100
@@ -20,6 +20,12 @@
     fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
              (map dest_Free (Misc_Legacy.term_frees t)) t
 
+fun add_final overloaded (c, T) thy =
+  let
+    val ctxt = Syntax.init_pretty_global thy;
+    val _ = Theory.check_overloading ctxt overloaded (c, T);
+  in Theory.add_deps ctxt "" (c, T) [] thy end;
+
 local
     fun mk_definitional [] arg = arg
       | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
@@ -58,8 +64,8 @@
                         val cdefname = if thname = ""
                                        then Thm.def_name (Long_Name.base_name cname)
                                        else thname
-                        val co = Const(cname_full,ctype)
-                        val thy' = Theory.add_finals_i covld [co] thy
+                        val thy' = add_final covld (cname_full,ctype) thy
+                        val co = Const (cname_full,ctype)
                         val tm' = case P of
                                       Abs(_, _, bodt) => subst_bound (co, bodt)
                                     | _ => P $ co
diff -r d68798000e46 -r 7ca3608146d8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Mar 16 22:31:19 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 16 22:48:38 2012 +0100
@@ -159,10 +159,6 @@
 
 val opt_overloaded = Parse.opt_keyword "overloaded";
 
-val _ =
-  Outer_Syntax.command ("finalconsts", Keyword.thy_decl) "declare constants as final"
-    (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
-
 val mode_spec =
   (Parse.$$$ "output" >> K ("", false)) ||
     Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
diff -r d68798000e46 -r 7ca3608146d8 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Mar 16 22:31:19 2012 +0100
+++ b/src/Pure/theory.ML	Fri Mar 16 22:48:38 2012 +0100
@@ -33,9 +33,8 @@
   val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
   val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
-  val add_finals_i: bool -> term list -> theory -> theory
-  val add_finals: bool -> string list -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
+  val check_overloading: Proof.context -> bool -> string * typ -> unit
 end
 
 structure Theory: THEORY =
@@ -267,28 +266,4 @@
 
 end;
 
-
-(* add_finals(_i) *)
-
-local
-
-fun gen_add_finals prep_term overloaded args thy =
-  let
-    val ctxt = Syntax.init_pretty_global thy;
-    fun const_of (Const const) = const
-      | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
-      | const_of _ = error "Attempt to finalize non-constant term";
-    fun specify (c, T) = dependencies ctxt false NONE (c ^ " axiom") (c, T) [];
-    val finalize =
-      specify o tap (check_overloading ctxt overloaded) o const_of o
-        Sign.cert_term thy o prep_term ctxt;
-  in thy |> map_defs (fold finalize args) end;
-
-in
-
-val add_finals_i = gen_add_finals (K I);
-val add_finals = gen_add_finals Syntax.read_term;
-
 end;
-
-end;