src/Provers/hypsubst.ML

--- a/src/Provers/hypsubst.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Provers/hypsubst.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -112,8 +112,8 @@
             orelse exists (curry Logic.occs (Free f)) ts
         then (orient, true) else raise Match
       | check_free ts (orient, _) = (orient, false)
-    fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
-      | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs =
+    fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
+      | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) hs =
               ((k, check_free (B :: hs) (inspect_pair bnd novars
                     (Data.dest_eq (Data.dest_Trueprop A))))
                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
@@ -227,7 +227,7 @@
     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
     if thin then thin_free_eq_tac ctxt else K no_tac];
 
-val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
+val hyp_subst_thin = Attrib.setup_config_bool \<^binding>\<open>hypsubst_thin\<close> (K false);
 
 fun hyp_subst_tac ctxt =
   hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
@@ -299,14 +299,14 @@
 
 val _ =
   Theory.setup
-   (Method.setup @{binding hypsubst}
+   (Method.setup \<^binding>\<open>hypsubst\<close>
       (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
       "substitution using an assumption (improper)" #>
-    Method.setup @{binding hypsubst_thin}
+    Method.setup \<^binding>\<open>hypsubst_thin\<close>
       (Scan.succeed (fn ctxt => SIMPLE_METHOD'
           (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
       "substitution using an assumption, eliminating assumptions" #>
-    Method.setup @{binding simplesubst}
+    Method.setup \<^binding>\<open>simplesubst\<close>
       (Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th)))
       "simple substitution");