src/HOL/Multivariate_Analysis/normarith.ML

      Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
    | _ => acc
  fun find_normedterms t acc = case term_of t of
     @{term "op + :: real => _"}$_$_ =>
             find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
-      | @{term "op * :: real => _"}$_$n =>
+      | @{term "op * :: real => _"}$_$_ =>
             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
             augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
                       (Thm.dest_arg t) acc
       | _ => augment_norm true t acc
 

     if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
  fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
 
+(*
  val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
+*)
  fun int_lincomb_cmul c t =
     if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
  fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+(*
  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
  fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
+*)
 
 fun vector_lincomb t = case term_of t of
    Const(@{const_name plus}, _) $ _ $ _ =>
     cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
  | Const(@{const_name minus}, _) $ _ $ _ =>

 fun replacenegnorms cv t = case term_of t of
   @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
 | @{term "op * :: real => _"}$_$_ =>
     if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
 | _ => Thm.reflexive t
+(*
 fun flip v eq =
   if FuncUtil.Ctermfunc.defined eq v
   then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
+*)
 fun allsubsets s = case s of
   [] => [[]]
 |(a::t) => let val res = allsubsets t in
                map (cons a) res @ res end
 fun evaluate env lin =

  val apply_pthc = rewrs_conv @{thms pth_c};
  val apply_pthd = try_conv (rewr_conv @{thm pth_d});
 
 fun headvector t = case t of
   Const(@{const_name plus}, _)$
-   (Const(@{const_name scaleR}, _)$l$v)$r => v
- | Const(@{const_name scaleR}, _)$l$v => v
+   (Const(@{const_name scaleR}, _)$_$v)$_ => v
+ | 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