src/HOL/Multivariate_Analysis/normarith.ML

   else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
                    (Numeral.mk_cnumber @{ctyp "real"} a))
         (Numeral.mk_cnumber @{ctyp "real"} b)
 end;
 
-fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
+fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
 
 fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
 
   (* I think here the static context should be sufficient!! *)
 fun inequality_canon_rule ctxt =

  let
 (*   val _ = error "real_vector_ineq_prover: pause" *)
   val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
   val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
-  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
+  fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
   fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
   val replace_conv = try_conv (rewrs_conv asl)
   val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))