src/HOL/Matrix_LP/Compute_Oracle/compute.ML

 fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab
 
 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
 
 val (_, export_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
+  (Thm.add_oracle (\<^binding>\<open>compute\<close>, fn (thy, hyps, shyps, prop) =>
     let
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
         fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))

              val (a, b) = Logic.dest_equals t
              val ty = type_of a
              val (encoding, a) = remove_types encoding a
              val (encoding, b) = remove_types encoding b
              val (eq, encoding) =
-              Encode.insert (Const (@{const_name Pure.eq}, ty --> ty --> @{typ "prop"})) encoding 
+              Encode.insert (Const (\<^const_name>\<open>Pure.eq\<close>, ty --> ty --> \<^typ>\<open>prop\<close>)) encoding 
          in
              (encoding, EqPrem (a, b, ty, eq))
          end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
     val (encoding, prems) = 
         (fold_rev (fn t => fn (encoding, l) => 

             val b' = run true b
         in
             case match_aterms varsubst b' a' of
                 NONE => 
                 let
-                    fun mk s = Syntax.string_of_term_global @{theory Pure}
+                    fun mk s = Syntax.string_of_term_global \<^theory>\<open>Pure\<close>
                       (infer_types (naming_of computer) (encoding_of computer) ty s)
                     val left = "computed left side: "^(mk a')
                     val right = "computed right side: "^(mk b')
                 in
                     raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")

 let
     val _ = check_compatible computer th
     val varsubst = varsubst_of_theorem th
     val encoding = encoding_of computer
     val naming = naming_of computer
-    fun infer t = infer_types naming encoding @{typ "prop"} t
+    fun infer t = infer_types naming encoding \<^typ>\<open>prop\<close> t
     fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t))
     fun runprem p = run (prem2term p)
     val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th))
     val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th)
     val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer))