insert now qualified and with authentic syntax

--- a/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
+++ b/src/HOL/Set.thy	Thu Jun 04 15:28:59 2009 +0200
@@ -20,7 +20,6 @@
 consts
   Collect       :: "('a => bool) => 'a set"              -- "comprehension"
   "op :"        :: "'a => 'a set => bool"                -- "membership"
-  insert        :: "'a => 'a set => 'a set"
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
   Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
@@ -58,19 +57,6 @@
 translations
   "{x. P}"      == "Collect (%x. P)"
 
-definition empty :: "'a set" ("{}") where
-  "empty \<equiv> {x. False}"
-
-definition UNIV :: "'a set" where
-  "UNIV \<equiv> {x. True}"
-
-syntax
-  "@Finset"     :: "args => 'a set"                       ("{(_)}")
-
-translations
-  "{x, xs}"     == "insert x {xs}"
-  "{x}"         == "insert x {}"
-
 definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
 
@@ -85,6 +71,22 @@
   "Int"  (infixl "\<inter>" 70) and
   "Un"  (infixl "\<union>" 65)
 
+definition empty :: "'a set" ("{}") where
+  "empty \<equiv> {x. False}"
+
+definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "insert a B \<equiv> {x. x = a} \<union> B"
+
+definition UNIV :: "'a set" where
+  "UNIV \<equiv> {x. True}"
+
+syntax
+  "@Finset"     :: "args => 'a set"                       ("{(_)}")
+
+translations
+  "{x, xs}"     == "CONST insert x {xs}"
+  "{x}"         == "CONST insert x {}"
+
 syntax
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
@@ -408,7 +410,6 @@
 
 defs
   Pow_def:      "Pow A          == {B. B <= A}"
-  insert_def:   "insert a B     == {x. x=a} Un B"
   image_def:    "f`A            == {y. EX x:A. y = f(x)}"
 
 
@@ -811,7 +812,7 @@
 by blast
 
 
-subsubsection {* Augmenting a set -- insert *}
+subsubsection {* Augmenting a set -- @{const insert} *}
 
 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
   by (unfold insert_def) blast

--- a/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
@@ -152,13 +152,13 @@
   let
     val sT = mk_setT T;
     val empty = Const ("Set.empty", sT);
-    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
+    fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
   in fold_rev insert ts empty end;
 
 fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
 
-fun dest_set (Const ("Orderings.bot", _)) = []
-  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
+fun dest_set (Const ("Set.empty", _)) = []
+  | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
   | dest_set t = raise TERM ("dest_set", [t]);
 
 fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);