# HG changeset patch # User haftmann # Date 1276269241 -7200 # Node ID 7c49988afd0e5d5c2bfe931b429b801f8e66dfe0 # Parent fe6262d929a3090133e14b5d8b213d3d6b0504f7 avoid references to old constdefs diff -r fe6262d929a3 -r 7c49988afd0e src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri Jun 11 17:14:01 2010 +0200 @@ -1946,7 +1946,7 @@ val p3 = string_of_mixfix csyn val p4 = smart_string_of_cterm crhs in - add_dump ("constdefs\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n " ^ p4) thy'' + add_dump ("definition\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n " ^ p4) thy'' end else add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^ @@ -2139,18 +2139,6 @@ end handle e => (message "exception in new_type_definition"; print_exn e) -fun add_dump_constdefs thy defname constname rhs ty = - let - val n = quotename constname - val t = Syntax.string_of_typ_global thy ty - val syn = string_of_mixfix (mk_syn thy constname) - (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*) - val eq = quote (constname ^ " == "^rhs) - val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : " - in - add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy - end - fun add_dump_syntax thy name = let val n = quotename name diff -r fe6262d929a3 -r 7c49988afd0e src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/refute.ML Fri Jun 11 17:14:01 2010 +0200 @@ -517,7 +517,7 @@ end (* ------------------------------------------------------------------------- *) -(* get_def: looks up the definition of a constant, as created by "constdefs" *) +(* get_def: looks up the definition of a constant *) (* ------------------------------------------------------------------------- *) (* theory -> string * Term.typ -> (string * Term.term) option *) @@ -711,7 +711,7 @@ (* Note: currently we use "inverse" functions to the definitional *) (* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) - (* "typedef", "constdefs". A more general approach could consider *) + (* "typedef", "definition". A more general approach could consider *) (* *every* axiom of the theory and collect it if it has a constant/ *) (* type/typeclass in common with the term 't'. *) diff -r fe6262d929a3 -r 7c49988afd0e src/ZF/ZF.thy --- a/src/ZF/ZF.thy Fri Jun 11 16:52:17 2010 +0200 +++ b/src/ZF/ZF.thy Fri Jun 11 17:14:01 2010 +0200 @@ -199,10 +199,7 @@ finalconsts 0 Pow Inf Union PrimReplace mem -defs -(*don't try to use constdefs: the declaration order is tightly constrained*) - - (* Bounded Quantifiers *) +defs (* Bounded Quantifiers *) Ball_def: "Ball(A, P) == \x. x\A --> P(x)" Bex_def: "Bex(A, P) == \x. x\A & P(x)"