--- a/doc-src/IsarRef/Thy/Spec.thy Wed Sep 08 10:45:55 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Wed Sep 08 13:22:24 2010 +0200
@@ -1069,7 +1069,6 @@
\begin{matharray}{rcl}
@{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -1079,18 +1078,6 @@
;
\end{rail}
- \begin{rail}
- 'constdefs' structs? (constdecl? constdef +)
- ;
-
- structs: '(' 'structure' (vars + 'and') ')'
- ;
- constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
- ;
- constdef: thmdecl? prop
- ;
- \end{rail}
-
\begin{description}
\item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
@@ -1111,25 +1098,6 @@
message would be issued for any definitional equation with a more
special type than that of the corresponding constant declaration.
- \item @{command "constdefs"} combines constant declarations and
- definitions, with type-inference taking care of the most general
- typing of the given specification (the optional type constraint may
- refer to type-inference dummies ``@{text _}'' as usual). The
- resulting type declaration needs to agree with that of the
- specification; overloading is \emph{not} supported here!
-
- The constant name may be omitted altogether, if neither type nor
- syntax declarations are given. The canonical name of the
- definitional axiom for constant @{text c} will be @{text c_def},
- unless specified otherwise. Also note that the given list of
- specifications is processed in a strictly sequential manner, with
- type-checking being performed independently.
-
- An optional initial context of @{text "(structure)"} declarations
- admits use of indexed syntax, using the special symbol @{verbatim
- "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
- particularly useful with locales (see also \secref{sec:locale}).
-
\end{description}
*}
--- a/src/Pure/IsaMakefile Wed Sep 08 10:45:55 2010 +0200
+++ b/src/Pure/IsaMakefile Wed Sep 08 13:22:24 2010 +0200
@@ -112,7 +112,6 @@
Isar/class.ML \
Isar/class_declaration.ML \
Isar/code.ML \
- Isar/constdefs.ML \
Isar/context_rules.ML \
Isar/element.ML \
Isar/expression.ML \
--- a/src/Pure/Isar/constdefs.ML Wed Sep 08 10:45:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(* Title: Pure/Isar/constdefs.ML
- Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
-
-Old-style constant definitions, with type-inference and optional
-structure context; specifications need to observe strictly sequential
-dependencies; no support for overloading.
-*)
-
-signature CONSTDEFS =
-sig
- val add_constdefs: (binding * string option) list *
- ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
- val add_constdefs_i: (binding * typ option) list *
- ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
-end;
-
-structure Constdefs: CONSTDEFS =
-struct
-
-(** add_constdefs(_i) **)
-
-fun gen_constdef prep_vars prep_prop prep_att
- structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
- let
- val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead";
-
- fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
-
- val thy_ctxt = ProofContext.init_global thy;
- val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
- val ((d, mx), var_ctxt) =
- (case raw_decl of
- NONE => ((NONE, NoSyn), struct_ctxt)
- | SOME raw_var =>
- struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
- ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
-
- val prop = prep_prop var_ctxt raw_prop;
- val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
- val _ =
- (case Option.map Name.of_binding d of
- NONE => ()
- | SOME c' =>
- if c <> c' then
- err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
- else ());
- val b = Binding.name c;
-
- val head = Const (Sign.full_bname thy c, T);
- val def = Term.subst_atomic [(Free (c, T), head)] prop;
- val name = Thm.def_binding_optional b raw_name;
- val atts = map (prep_att thy) raw_atts;
-
- val thy' =
- thy
- |> Sign.add_consts_i [(b, T, mx)]
- |> PureThy.add_defs false [((name, def), atts)]
- |-> (fn [thm] => (* FIXME thm vs. atts !? *)
- Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
- Code.add_default_eqn thm);
- in ((c, T), thy') end;
-
-fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
- let
- val ctxt = ProofContext.init_global thy;
- val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
- val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
- in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
-
-val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
-val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
-
-end;
--- a/src/Pure/Isar/isar_syn.ML Wed Sep 08 10:45:55 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Sep 08 13:22:24 2010 +0200
@@ -203,25 +203,6 @@
>> (Toplevel.theory o Isar_Cmd.add_defs));
-(* old constdefs *)
-
-val old_constdecl =
- Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) ||
- Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix'
- --| Scan.option Parse.where_ >> Parse.triple1 ||
- Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
-
-val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop);
-
-val structs =
- Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
- |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
-
-val _ =
- Outer_Syntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
- (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
-
-
(* constant definitions and abbreviations *)
val _ =
--- a/src/Pure/ROOT.ML Wed Sep 08 10:45:55 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Sep 08 13:22:24 2010 +0200
@@ -226,7 +226,6 @@
use "Isar/spec_rules.ML";
use "Isar/specification.ML";
use "Isar/typedecl.ML";
-use "Isar/constdefs.ML";
(*toplevel transactions*)
use "Thy/thy_load.ML";