src/HOL/Tools/TFL/usyntax.ML

   | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
 
 
 fun mk_imp{ant,conseq} =
-   let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[ant,conseq])
    end;
 
 fun mk_select (r as {Bvar,Body}) =
   let val ty = type_of Bvar

   in list_comb(c,[mk_abs r])
   end;
 
 fun mk_forall (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
+      val c = Const(@{const_name "All"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   in list_comb(c,[mk_abs r])
   end;
 
 fun mk_exists (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
+      val c = Const(@{const_name "Ex"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   in list_comb(c,[mk_abs r])
   end;
 
 
 fun mk_conj{conj1,conj2} =
-   let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[conj1,conj2])
    end;
 
 fun mk_disj{disj1,disj2} =
-   let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[disj1,disj2])
    end;
 
 fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
 

        val v = Free(s', ty);
      in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
      end
   | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
 
-fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
+fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
   | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
 
-fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
   | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
 
-fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_forall(Const(@{const_name "All"},_) $ (a as Abs _)) = fst (dest_abs [] a)
   | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
 
-fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_exists(Const(@{const_name "Ex"},_) $ (a as Abs _)) = fst (dest_abs [] a)
   | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
 
 fun dest_neg(Const("not",_) $ M) = M
   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
 
-fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
   | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
 
-fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
   | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
 
 fun mk_pair{fst,snd} =
    let val ty1 = type_of fst
        val ty2 = type_of snd

 
 fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
-                       Body=Const("True",HOLogic.boolT)};
+                       Body=Const(@{const_name "True"},HOLogic.boolT)};
 
 end;