diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -238,7 +238,7 @@
   if is_binop ct ct' then Thm.dest_binop ct'
   else raise CTERM ("dest_binop: bad binop", [ct, ct'])
 
-fun inst_thm inst = Thm.instantiate ([], inst);
+fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst);
 
 val dest_number = Thm.term_of #> HOLogic.dest_number #> snd;
 val is_number = can dest_number;
@@ -300,7 +300,7 @@
         val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
         val neg_tm = Thm.dest_fun neg_pat
         val dest_sub = dest_binop sub_tm
-      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub, neg_mul |> concl |> Thm.dest_arg,
+      in (neg_mul, sub_add, sub_tm, neg_tm, dest_sub, neg_mul |> concl |> Thm.dest_arg,
           sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
       end
     | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), true_tm, true_tm));
@@ -760,7 +760,7 @@
 fun polynomial_neg_conv ctxt tm =
    let val (l,r) = Thm.dest_comb tm in
         if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
-        let val th1 = inst_thm [(cx',r)] neg_mul
+        let val th1 = inst_thm [(cx', r)] neg_mul
             val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
         in Thm.transitive th2 (polynomial_monomial_mul_conv ctxt (concl th2))
         end
@@ -770,7 +770,7 @@
 (* Subtraction.                                                              *)
 fun polynomial_sub_conv ctxt tm =
   let val (l,r) = dest_sub tm
-      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
+      val th1 = inst_thm [(cx', l), (cy', r)] sub_add
       val (tm1,tm2) = Thm.dest_comb(concl th1)
       val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv ctxt tm2)
   in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv ctxt (concl th2)))