src/ZF/Tools/primrec_package.ML

     fun add_case ((cname, recursor_pair), cases) =
       let val (rhs, recursor_rhs, eq) =
             case AList.lookup (op =) eqns cname of
                 NONE => (warning ("no equation for constructor " ^ cname ^
                                   "\nin definition of function " ^ fname);
-                         (Const (@{const_name zero}, Ind_Syntax.iT),
-                          #2 recursor_pair, Const (@{const_name zero}, Ind_Syntax.iT)))
+                         (Const (\<^const_name>\<open>zero\<close>, Ind_Syntax.iT),
+                          #2 recursor_pair, Const (\<^const_name>\<open>zero\<close>, Ind_Syntax.iT)))
               | SOME (rhs, cargs', eq) =>
                     (rhs, inst_recursor (recursor_pair, cargs'), eq)
           val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
           val abs = List.foldr absterm rhs allowed_terms
       in

 
 
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
+  Outer_Syntax.command \<^command_keyword>\<open>primrec\<close> "define primitive recursive functions on datatypes"
     (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
       >> (Toplevel.theory o (#1 oo (primrec o map (fn ((x, y), z) => ((x, z), y))))));
 
 end;