src/HOL/Library/normarith.ML

 fun inequality_canon_rule ctxt = 
  let 
   (* FIXME : Should be computed statically!! *)
   val real_poly_conv = 
     Normalizer.semiring_normalize_wrapper ctxt
-     (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+     (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
  in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv)))
 end;
 
  fun absc cv ct = case term_of ct of 
  Abs (v,_, _) => 

  fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 
   let 
    (* FIXME: Should be computed statically!!*)
    val real_poly_conv = 
       Normalizer.semiring_normalize_wrapper ctxt
-       (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+       (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
    val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
    val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
            else ()
    val dests = distinct (op aconvc) (map snd rawdests)

   (* FIXME: Lookup in the context every time!!! Fix this !!!*)
  fun splitequation ctxt th acc =
   let 
    val real_poly_neg_conv = #neg
        (Normalizer.semiring_normalizers_ord_wrapper ctxt
-        (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
+        (the (NormalizerData.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
   end
 in fun real_vector_prover ctxt _ translator (eqs,ges,gts) =
      (real_vector_ineq_prover ctxt translator