# HG changeset patch # User haftmann # Date 1283944944 -7200 # Node ID 49fc6c842d6cdbec4cb489f7a25add57661f2faf # Parent 297cd703f1f0738f63d3a06678f522d584d33675 removed ancient constdefs command diff -r 297cd703f1f0 -r 49fc6c842d6c doc-src/IsarRef/Thy/Spec.thy --- 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 \ theory"} \\ @{command_def "defs"} & : & @{text "theory \ theory"} \\ - @{command_def "constdefs"} & : & @{text "theory \ 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 :: \"} 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 - "\"} (printed as ``@{text "\"}''). The latter concept is - particularly useful with locales (see also \secref{sec:locale}). - \end{description} *} diff -r 297cd703f1f0 -r 49fc6c842d6c src/Pure/IsaMakefile --- 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 \ diff -r 297cd703f1f0 -r 49fc6c842d6c src/Pure/Isar/constdefs.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; diff -r 297cd703f1f0 -r 49fc6c842d6c src/Pure/Isar/isar_syn.ML --- 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 _ = diff -r 297cd703f1f0 -r 49fc6c842d6c src/Pure/ROOT.ML --- 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";