src/HOL/Tools/Function/termination.ML

 fun mk_sum_skel rel =
   let
     val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
     fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
-        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+        val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
           = Term.strip_qnt_body "Ex" c
       in cons r o cons l end
   in
     mk_skel (fold collect_pats cs [])
   end

   let
     val (sk, _, _, _, _) = D
     val vs = Term.strip_qnt_vars "Ex" c
 
     (* FIXME: throw error "dest_call" for malformed terms *)
-    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+    val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
       = Term.strip_qnt_body "Ex" c
     val (p, l') = dest_inj sk l
     val (q, r') = dest_inj sk r
   in
     (vs, p, l', q, r', Gam)