src/HOL/Decision_Procs/langford.ML

 
 val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
 
 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
  case term_of ep of 
-  Const("Ex",_)$_ => 
+  Const(@{const_name "Ex"},_)$_ => 
    let 
      val p = Thm.dest_arg ep
      val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
      val (L,U) = 
        let 

  in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
 
 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
 
 fun is_eqx x eq = case term_of eq of
-   Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
+   Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
  | _ => false ;
 
 local 
 fun proc ct = 
  case term_of ct of
-  Const("Ex",_)$Abs (xn,_,_) => 
+  Const(@{const_name "Ex"},_)$Abs (xn,_,_) => 
    let 
     val e = Thm.dest_fun ct
     val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
     val Pp = Thm.capply @{cterm "Trueprop"} p 
     val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)

 
 val grab_atom_bop =
  let
   fun h bounds tm =
    (case term_of tm of
-     Const ("op =", T) $ _ $ _ =>
+     Const (@{const_name "op ="}, T) $ _ $ _ =>
        if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
-   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
-   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
+   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
+   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const ("op &", _) $ _ $ _ => find_args bounds tm
-   | Const ("op |", _) $ _ $ _ => find_args bounds tm
-   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
-   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
+   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
   and find_args bounds tm =
     (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
  and find_body bounds b =
    let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b