diff -r 19b47bfac6ef -r 9e7d1c139569 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -165,7 +165,9 @@
   val real_poly_conv =
     Semiring_Normalizer.semiring_normalize_wrapper ctxt
      (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
- in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv)))
+ in
+  fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv
+    arg_conv (Numeral_Simprocs.field_comp_conv ctxt then_conv real_poly_conv)))
 end;
 
  val apply_pth1 = rewr_conv @{thm pth_1};
@@ -175,8 +177,13 @@
  val apply_pth5 = rewr_conv @{thm pth_5};
  val apply_pth6 = rewr_conv @{thm pth_6};
  val apply_pth7 = rewrs_conv @{thms pth_7};
- val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Numeral_Simprocs.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
- val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Numeral_Simprocs.field_comp_conv);
+ fun apply_pth8 ctxt =
+  rewr_conv @{thm pth_8} then_conv
+  arg1_conv (Numeral_Simprocs.field_comp_conv ctxt) then_conv
+  (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
+ fun apply_pth9 ctxt =
+  rewrs_conv @{thms pth_9} then_conv
+  arg1_conv (arg1_conv (Numeral_Simprocs.field_comp_conv ctxt));
  val apply_ptha = rewr_conv @{thm pth_a};
  val apply_pthb = rewrs_conv @{thms pth_b};
  val apply_pthc = rewrs_conv @{thms pth_c};
@@ -188,13 +195,13 @@
  | Const(@{const_name scaleR}, _)$_$v => v
  | _ => error "headvector: non-canonical term"
 
-fun vector_cmul_conv ct =
-   ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv
-    (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct
+fun vector_cmul_conv ctxt ct =
+   ((apply_pth5 then_conv arg1_conv (Numeral_Simprocs.field_comp_conv ctxt)) else_conv
+    (apply_pth6 then_conv binop_conv (vector_cmul_conv ctxt))) ct
 
-fun vector_add_conv ct = apply_pth7 ct
+fun vector_add_conv ctxt ct = apply_pth7 ct
  handle CTERM _ =>
-  (apply_pth8 ct
+  (apply_pth8 ctxt ct
    handle CTERM _ =>
     (case term_of ct of
      Const(@{const_name plus},_)$lt$rt =>
@@ -202,35 +209,35 @@
        val l = headvector lt
        val r = headvector rt
       in (case Term_Ord.fast_term_ord (l,r) of
-         LESS => (apply_pthb then_conv arg_conv vector_add_conv
+         LESS => (apply_pthb then_conv arg_conv (vector_add_conv ctxt)
                   then_conv apply_pthd) ct
-        | GREATER => (apply_pthc then_conv arg_conv vector_add_conv
+        | GREATER => (apply_pthc then_conv arg_conv (vector_add_conv ctxt)
                      then_conv apply_pthd) ct
-        | EQUAL => (apply_pth9 then_conv
-                ((apply_ptha then_conv vector_add_conv) else_conv
-              arg_conv vector_add_conv then_conv apply_pthd)) ct)
+        | EQUAL => (apply_pth9 ctxt then_conv
+                ((apply_ptha then_conv (vector_add_conv ctxt)) else_conv
+              arg_conv (vector_add_conv ctxt) then_conv apply_pthd)) ct)
       end
      | _ => Thm.reflexive ct))
 
-fun vector_canon_conv ct = case term_of ct of
+fun vector_canon_conv ctxt ct = case term_of ct of
  Const(@{const_name plus},_)$_$_ =>
   let
    val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb
-   val lth = vector_canon_conv l
-   val rth = vector_canon_conv r
+   val lth = vector_canon_conv ctxt l
+   val rth = vector_canon_conv ctxt r
    val th = Drule.binop_cong_rule p lth rth
-  in fconv_rule (arg_conv vector_add_conv) th end
+  in fconv_rule (arg_conv (vector_add_conv ctxt)) th end
 
 | Const(@{const_name scaleR}, _)$_$_ =>
   let
    val (p,r) = Thm.dest_comb ct
-   val rth = Drule.arg_cong_rule p (vector_canon_conv r)
-  in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth
+   val rth = Drule.arg_cong_rule p (vector_canon_conv ctxt r)
+  in fconv_rule (arg_conv (apply_pth4 else_conv (vector_cmul_conv ctxt))) rth
   end
 
-| Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv vector_canon_conv) ct
+| Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv (vector_canon_conv ctxt)) ct
 
-| Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct
+| Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv (vector_canon_conv ctxt)) ct
 
 (* FIXME
 | Const(@{const_name vec},_)$n =>
@@ -241,8 +248,8 @@
 *)
 | _ => apply_pth1 ct
 
-fun norm_canon_conv ct = case term_of ct of
-  Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
+fun norm_canon_conv ctxt ct = case term_of ct of
+  Const(@{const_name norm},_)$_ => arg_conv (vector_canon_conv ctxt) ct
  | _ => raise CTERM ("norm_canon_conv", [ct])
 
 fun int_flip v eq =
@@ -314,9 +321,9 @@
   in fst (RealArith.real_linear_prover translator
         (map (fn t => Drule.instantiate_normalize ([(tv_n, ctyp_of_term t)],[]) pth_zero)
             zerodests,
-        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
+        map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
-        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
+        map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) gts))
   end
 in val real_vector_combo_prover = real_vector_combo_prover
@@ -367,7 +374,7 @@
        (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
         (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    val (th1,th2) = conj_pair(rawrule th)
-  in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
+  in th1::fconv_rule (arg_conv (arg_conv (real_poly_neg_conv ctxt))) th2::acc
   end
 in fun real_vector_prover ctxt _ translator (eqs,ges,gts) =
      (real_vector_ineq_prover ctxt translator
@@ -375,10 +382,11 @@
 end;
 
   fun init_conv ctxt =
-   Simplifier.rewrite (Simplifier.context ctxt
-     (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
-   then_conv Numeral_Simprocs.field_comp_conv
-   then_conv nnf_conv
+   Simplifier.rewrite (put_simpset HOL_basic_ss ctxt
+    addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus},
+      @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))
+   then_conv Numeral_Simprocs.field_comp_conv ctxt
+   then_conv nnf_conv ctxt
 
  fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
  fun norm_arith ctxt ct =