src/HOL/Tools/inductive_set.ML

 
 (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
 
 val collect_mem_simproc =
   Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
-    fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
+    fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
          let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
-           (c as Const ("op :", _)) $ q $ S' =>
+           (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
              (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
                   if not (loose_bvar (S', 0)) andalso
                     ts = map Bound (length ps downto 0)

       fun close p t f =
         let val vs = Term.add_vars t []
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
-        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
+      fun mkop @{const_name "op &"} T x =
+            SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
+        | mkop @{const_name "op |"} T x =
+            SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T
         in HOLogic.Collect_const U $
           HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
         end;
-      fun decomp (Const (s, _) $ ((m as Const ("op :",
+      fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
             Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
               mkop s T (m, p, S, mk_collect p T (head_of u))
-        | decomp (Const (s, _) $ u $ ((m as Const ("op :",
+        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
             Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
               mkop s T (m, p, mk_collect p T (head_of u), S)
         | decomp _ = NONE;
       val simp = full_simp_tac (Simplifier.inherit_context ss
         (HOL_basic_ss addsimps [mem_Collect_eq, split_conv])) 1;

 
 (**** declare rules for converting predicates to sets ****)
 
 fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
   case prop_of thm of
-    Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) =>
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
       (case body_type T of
-         Type ("bool", []) =>
+         @{typ bool} =>
            let
              val thy = Context.theory_of ctxt;
              fun factors_of t fs = case strip_abs_body t of
-                 Const ("op :", _) $ u $ S =>
+                 Const (@{const_name "op :"}, _) $ u $ S =>
                    if is_Free S orelse is_Var S then
                      let val ps = HOLogic.flat_tuple_paths u
                      in (SOME ps, (S, ps) :: fs) end
                    else (NONE, fs)
                | _ => (NONE, fs);
              val (h, ts) = strip_comb lhs
              val (pfs, fs) = fold_map factors_of ts [];
              val ((h', ts'), fs') = (case rhs of
                  Abs _ => (case strip_abs_body rhs of
-                     Const ("op :", _) $ u $ S =>
+                     Const (@{const_name "op :"}, _) $ u $ S =>
                        (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
                    | _ => error "member symbol on right-hand side expected")
                | _ => (strip_comb rhs, NONE))
            in
              case (name_type_of h, name_type_of h') of

   let
     val thy = ProofContext.theory_of lthy;
     val {set_arities, pred_arities, to_pred_simps, ...} =
       PredSetConvData.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t
-      | infer (Const ("op :", _) $ t $ u) =
+      | infer (Const (@{const_name "op :"}, _) $ t $ u) =
           infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
       | infer (t $ u) = infer t #> infer u
       | infer _ = I;
     val new_arities = filter_out
       (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1