# HG changeset patch
# User berghofe
# Date 1120219378 -7200
# Node ID 3dc904d93767fa1a8783df2eeb1f7eb0e81738cc
# Parent  62dff56b43d3fc0693122d2611dece708694e7c4
Removed setsubgoaler hack.

diff -r 62dff56b43d3 -r 3dc904d93767 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jul 01 14:01:13 2005 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Jul 01 14:02:58 2005 +0200
@@ -301,18 +301,10 @@
   "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
-ML_setup {* 
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in comm_monoid) finprod_empty [simp]: 
   "finprod G f {} = \<one>"
   by (simp add: finprod_def)
 
-ML_setup {* 
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
 declare funcsetI [intro]
   funcset_mem [dest]