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