# HG changeset patch
# User wenzelm
# Date 1213478406 -7200
# Node ID 0978b8e32fd0395d3fcfd72d2bff623f8906508e
# Parent  2c7a628ccdcfa83afab58d4d2f450d9c1e509b7a
tuned proof;

diff -r 2c7a628ccdcf -r 0978b8e32fd0 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Sat Jun 14 23:20:05 2008 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Sat Jun 14 23:20:06 2008 +0200
@@ -138,18 +138,17 @@
   apply simp
   done
 
-ML {* simplify (@{simpset} addsimps [thm "eucl_size_def"]
-    delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *}
-
-thm long_div_eucl_size [simplified]
+ML {*
+ bind_thm ("long_div_ring_aux",
+    simplify (@{simpset} addsimps [@{thm eucl_size_def}]
+    delsimprocs [ring_simproc]) (@{thm long_div_eucl_size}))
+*}
 
 lemma long_div_ring: 
   "!!g::('a::ring up). g ~= 0 ==>  
      Ex (% (q, r, k).  
        (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
-  apply (tactic {* forw_inst_tac [("f", "f")]
-    (simplify (@{simpset} addsimps [thm "eucl_size_def"]
-      delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *})
+  apply (frule_tac f = f in long_div_ring_aux)
   apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *})
   apply (case_tac "aa = 0")
    apply blast