src/Pure/Isar/theory_target.ML

     (* FIXME !? *)
     val mx' = if is_class lthy then NoSyn else Syntax.unlocalize_mixfix is_loc mx;
   in
     lthy1
     |> LocalTheory.theory (Sign.add_notation prmode [(v', mx')])
-    |> is_loc ? internal_abbrev (PolyML.print ((c, mx), Term.list_comb (v, xs)))
+    |> is_loc ? internal_abbrev ((c, mx), Term.list_comb (v, xs))
   end;
 
 
 (* consts *)