--- a/src/HOL/Multivariate_Analysis/normarith.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Mon Jul 27 17:44:55 2015 +0200
@@ -154,7 +154,7 @@
(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};
@@ -342,7 +342,7 @@
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