# 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) == \<forall>x. x\<in>A --> P(x)"
   Bex_def:       "Bex(A, P) == \<exists>x. x\<in>A & P(x)"