src/HOL/Hoare/hoare_tac.ML

--- a/src/HOL/Hoare/hoare_tac.ML	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Sat Jan 05 17:24:33 2019 +0100
@@ -26,12 +26,12 @@
 local
 
 (** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (\<^const_name>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
 (** maps {(x1,...,xn). t} to [x1,...,xn] **)
-fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T
+fun mk_vars (Const (\<^const_name>\<open>Collect\<close>,_) $ T) = abs2list T
   | mk_vars _ = [];
 
 (** abstraction of body over a tuple formed from a list of free variables.
@@ -47,7 +47,7 @@
             Abs (_, T, _) => T
           | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
       in
-        Const (@{const_name case_prod},
+        Const (\<^const_name>\<open>case_prod\<close>,
             (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
           absfree (x, T) z
       end;
@@ -62,8 +62,8 @@
         val T2 =
           (case z of
             Free (_, T) => T
-          | Const (@{const_name Pair}, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
-     in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
+          | Const (\<^const_name>\<open>Pair\<close>, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
+     in Const (\<^const_name>\<open>Pair\<close>, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
 
 (** maps a subgoal of the form:
     VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
@@ -78,7 +78,7 @@
   let val T as Type ("fun",[t,_]) = fastype_of tm;
   in HOLogic.Collect_const t $ tm end;
 
-fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT);
+fun inclt ty = Const (\<^const_name>\<open>Orderings.less_eq\<close>, [ty,ty] ---> HOLogic.boolT);
 
 in