--- a/src/HOL/Library/normarith.ML Thu Jun 04 14:32:00 2009 -0700
+++ b/src/HOL/Library/normarith.ML Thu Jun 04 16:11:36 2009 -0700
@@ -353,7 +353,7 @@
val ntms = fold_rev find_normedterms (map (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 mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t
+ fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
val replace_conv = try_conv (rewrs_conv asl)