src/Pure/Syntax/syntax_trans.ML

 fun bigimpl_ast_tr (asts as [asms, concl]) =
       let val prems =
         (case Ast.unfold_ast_p "_asms" asms of
           (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
         | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
-      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
+      in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
   | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
 
 
 (* type/term reflection *)
 

 (* meta implication *)
 
 fun impl_ast_tr' asts =
   if no_brackets () then raise Match
   else
-    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
+    (case Ast.unfold_ast_p "\\<^const>Pure.imp"
+        (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
       (prems as _ :: _ :: _, concl) =>
         let
           val (asms, asm) = split_last prems;
           val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
         in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end

 val pure_print_ast_translation =
  [("\\<^type>fun", fn _ => fun_ast_tr'),
   ("_abs", fn _ => abs_ast_tr'),
   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
-  ("\\<^const>==>", fn _ => impl_ast_tr'),
+  ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
   ("_index", fn _ => index_ast_tr')];
 
 end;
 
 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;