tuned;

--- a/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 10:40:53 2016 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 10:42:53 2016 +0200
@@ -137,7 +137,7 @@
         val frees = fold Term.add_frees pat []
         val abs_rhs = fold absfree frees rhs
         val ([(f, (_, def))], lthy') = lthy
-          |> Local_Defs.define [((Binding.name name, Mixfix.NoSyn), (Thm.empty_binding, abs_rhs))]
+          |> Local_Defs.define [((Binding.name name, NoSyn), (Thm.empty_binding, abs_rhs))]
       in ((list_comb (f, map Free (rev frees)), def), lthy') end
 
     val ((def_ts, def_thms), ctxt2) =

--- a/src/Pure/Syntax/syntax.ML	Wed Jun 22 10:40:53 2016 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Jun 22 10:42:53 2016 +0200
@@ -612,9 +612,9 @@
 fun guess_infix (Syntax ({gram, ...}, _)) c =
   (case Parser.guess_infix_lr (Lazy.force gram) c of
     SOME (s, l, r, j) => SOME
-     (if l then Mixfix.Infixl (Input.string s, j, Position.no_range)
-      else if r then Mixfix.Infixr (Input.string s, j, Position.no_range)
-      else Mixfix.Infix (Input.string s, j, Position.no_range))
+     (if l then Infixl (Input.string s, j, Position.no_range)
+      else if r then Infixr (Input.string s, j, Position.no_range)
+      else Infix (Input.string s, j, Position.no_range))
   | NONE => NONE);