src/FOLP/hypsubst.ML

 
 (*Locates a substitutable variable on the left (resp. right) of an equality
    assumption.  Returns the number of intervening assumptions, paried with
    the rule asm_rl (resp. sym). *)
 fun eq_var bnd =
-  let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
-        | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
+  let fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) = eq_var_aux k t
+        | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) =
               ((k, inspect_pair bnd (dest_eq A))
                       (*Exception Match comes from inspect_pair or dest_eq*)
                handle Match => eq_var_aux (k+1) B)
         | eq_var_aux k _ = raise EQ_VAR
   in  eq_var_aux 0  end;