--- a/src/FOLP/hypsubst.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/FOLP/hypsubst.ML Fri Jan 04 23:22:53 2019 +0100
@@ -58,8 +58,8 @@
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)