--- a/src/HOL/Algebra/FiniteProduct.thy Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Apr 16 13:52:43 2004 +0200
@@ -291,8 +291,7 @@
like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
ML_setup {*
- Context.>> (fn thy => (simpset_ref_of thy :=
- simpset_of thy setsubgoaler asm_full_simp_tac; thy))
+ simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
*}
lemma (in comm_monoid) finprod_empty [simp]:
@@ -300,8 +299,7 @@
by (simp add: finprod_def)
ML_setup {*
- Context.>> (fn thy => (simpset_ref_of thy :=
- simpset_of thy setsubgoaler asm_simp_tac; thy))
+ simpset_ref() := simpset() setsubgoaler asm_simp_tac;
*}
declare funcsetI [intro]