src/Pure/Isar/local_defs.ML

 val head_of_def =
   Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
 
 
 (*
-  [x, x == a]
+  [x, x \<equiv> a]
        :
       B x
   -----------
       B a
 *)

 
 
 (* specific export -- result based on educated guessing *)
 
 (*
-  [xs, xs == as]
+  [xs, xs \<equiv> as]
         :
        B xs
   --------------
        B as
 *)

                   else (Drule.abs_def (Variable.gen_all outer asm), true))
             end)));
   in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
 
 (*
-  [xs, xs == as]
+  [xs, xs \<equiv> as]
         :
      TERM b xs
   --------------  and  --------------
-     TERM b as          b xs == b as
+     TERM b as          b xs \<equiv> b as
 *)
 fun export_cterm inner outer ct =
   export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
 
 fun contract ctxt defs ct th =