src/HOL/Tools/Function/termination.ML

           in dest s l @ dest t r end
   in dest end
 
 
 (* concrete versions for sum types *)
-fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
-  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
+  | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
   | is_inj _ = false
 
-fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
   | dest_inl _ = NONE
 
-fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
   | dest_inr _ = NONE
 
 
 fun mk_skel ps =
   let

           sk
   |> fst
 
 fun mk_sum_skel rel =
   let
-    val cs = FundefLib.dest_binop_list @{const_name union} rel
-    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+    fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
         val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
           = Term.strip_qnt_body "Ex" c
       in cons r o cons l end
   in

   Term2tab.lookup C (c1, c2)
 
 fun get_descent (_, _, _, _, D) c m1 m2 =
   Term3tab.lookup D (c, (m1, m2))
 
-fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   let
     val n = get_num_points D
     val (sk, _, _, _, _) = D
     val vs = Term.strip_qnt_vars "Ex" c
 

   end
 
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st
   else case Thm.term_of (Thm.cprem_of st i) of
-    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
+    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   |_ => no_tac st
 
 type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
 
 fun TERMINATION ctxt tac =
-  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+  SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
   let
     val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
   in
     tac (create ctxt T rel) i
   end)

 
       val relation =
           if null ineqs then
               Const (@{const_name Set.empty}, fastype_of rel)
           else
-              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
+              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
 
       fun solve_membership_tac i =
           (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
           THEN' (fn j => TRY (rtac @{thm UnI1} j))
           THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)