# HG changeset patch
# User wenzelm
# Date 1267300628 -3600
# Node ID 115a5a95710a4da36be0624f8ff73938b6cb2193
# Parent  bfcbab8592ba8e85d4191ddaf746a8c1b82a4083
clarified @{const_name} vs. @{const_abbrev};

diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Feb 27 20:57:08 2010 +0100
@@ -1631,9 +1631,9 @@
 
 setup {*
 let
-  fun msetT T = Type ("Multiset.multiset", [T]);
+  fun msetT T = Type (@{type_name multiset}, [T]);
 
-  fun mk_mset T [] = Const (@{const_name Mempty}, msetT T)
+  fun mk_mset T [] = Const (@{const_abbrev Mempty}, msetT T)
     | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
     | mk_mset T (x :: xs) =
           Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
@@ -1649,7 +1649,7 @@
       rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
 
   val regroup_munion_conv =
-      Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+      Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
         (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
 
   fun unfold_pwleq_tac i =
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -1016,7 +1016,7 @@
               (HOLogic.mk_Trueprop (HOLogic.mk_eq
                 (supp c,
                  if null dts then HOLogic.mk_set atomT []
-                 else foldr1 (HOLogic.mk_binop @{const_name union}) (map supp args2)))))
+                 else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Rat.thy	Sat Feb 27 20:57:08 2010 +0100
@@ -1188,7 +1188,7 @@
     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
-    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
+    (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
 *}
 
 lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -465,7 +465,7 @@
           (if i < length newTs then HOLogic.true_const
            else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
              Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
-               Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
+               Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
       end;
 
     val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -168,7 +168,7 @@
 
 (* instance for unions *)
 val regroup_union_conv =
-  regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
+  regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup}
     (map (fn t => t RS eq_reflection)
       (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left}))
 
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -24,7 +24,7 @@
   let
     val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
     val mlexT = (domT --> HOLogic.natT) --> relT --> relT
-    fun mk_ms [] = Const (@{const_name Set.empty}, relT)
+    fun mk_ms [] = Const (@{const_abbrev Set.empty}, relT)
       | mk_ms (f::fs) =
         Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
   in
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -286,7 +286,7 @@
 
     val relation =
       if null ineqs
-      then Const (@{const_name Set.empty}, fastype_of rel)
+      then Const (@{const_abbrev Set.empty}, fastype_of rel)
       else map mk_compr ineqs
         |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
 
@@ -321,7 +321,7 @@
   let
     val goal =
       HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
-        Const (@{const_name Set.empty}, fastype_of c1))
+        Const (@{const_abbrev Set.empty}, fastype_of c1))
       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   in
     case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -283,7 +283,7 @@
     (* bool -> typ -> typ -> (term * term) list -> term *)
     fun make_set maybe_opt T1 T2 tps =
       let
-        val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
+        val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
         val insert_const = Const (@{const_name insert},
                                   T1 --> (T1 --> T2) --> T1 --> T2)
         (* (term * term) list -> term *)
@@ -313,7 +313,7 @@
         val update_const = Const (@{const_name fun_upd},
                                   (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
         (* (term * term) list -> term *)
-        fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
+        fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
           | aux' ((t1, t2) :: ps) =
             (case t2 of
                Const (@{const_name None}, _) => aux' ps
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -2933,7 +2933,7 @@
             "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
   in
     if k = ~1 orelse length ts < k then elems
-      else Const (@{const_name Set.union}, setT --> setT --> setT) $ elems $ cont
+      else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont
   end;
 
 fun values_cmd print_modes param_user_modes options k raw_t state =
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -265,7 +265,7 @@
   | is_eq _ = false
 
 fun mk_rel_compose (trm1, trm2) =
-  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
+  Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
 let
diff -r bfcbab8592ba -r 115a5a95710a src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Feb 27 20:56:03 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Feb 27 20:57:08 2010 +0100
@@ -510,7 +510,7 @@
 val setup =
   Attrib.setup @{binding ind_realizer}
     ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
-      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
+      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
     "add realizers for inductive set";
 
 end;