# HG changeset patch
# User wenzelm
# Date 1273940150 -7200
# Node ID 897ee863885dc88f6d6ad3133493ef4cb79d7a05
# Parent  278029c8a4622232a0112ecf232db7ffd04fbe79
removed unused conversions;

diff -r 278029c8a462 -r 897ee863885d src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Sat May 15 18:12:58 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat May 15 18:15:50 2010 +0200
@@ -169,17 +169,6 @@
  in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv)))
 end;
 
- fun absc cv ct = case term_of ct of
- Abs (v,_, _) =>
-  let val (x,t) = Thm.dest_abs (SOME v) ct
-  in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
-  end
- | _ => all_conv ct;
-
-fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct;
-fun botc1 conv ct =
-  ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct;
-
  val apply_pth1 = rewr_conv @{thm pth_1};
  val apply_pth2 = rewr_conv @{thm pth_2};
  val apply_pth3 = rewr_conv @{thm pth_3};