# HG changeset patch
# User webertj
# Date 1154217961 -7200
# Node ID 5a8410198a33dd4f68b9890ac547e01c7b57ea77
# Parent  58b71535ed0089c928739c10ec457ed353961f08
bugfix related to cancel_div_mod simproc

diff -r 58b71535ed00 -r 5a8410198a33 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Sat Jul 29 13:15:12 2006 +0200
+++ b/src/HOL/Integ/presburger.ML	Sun Jul 30 02:06:01 2006 +0200
@@ -289,7 +289,7 @@
     (* Transform the term*)
     val (t,np,nh) = prepare_for_presburger sg q g'
     (* Some simpsets for dealing with mod div abs and nat*)
-    val mod_div_simpset = HOL_basic_ss 
+    val mod_div_simpset = Simplifier.theory_context sg HOL_basic_ss
 			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
 				  nat_mod_add_right_eq, int_mod_add_eq, 
 				  int_mod_add_right_eq, int_mod_add_left_eq,
diff -r 58b71535ed00 -r 5a8410198a33 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Sat Jul 29 13:15:12 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sun Jul 30 02:06:01 2006 +0200
@@ -289,7 +289,7 @@
     (* Transform the term*)
     val (t,np,nh) = prepare_for_presburger sg q g'
     (* Some simpsets for dealing with mod div abs and nat*)
-    val mod_div_simpset = HOL_basic_ss 
+    val mod_div_simpset = Simplifier.theory_context sg HOL_basic_ss
 			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
 				  nat_mod_add_right_eq, int_mod_add_eq, 
 				  int_mod_add_right_eq, int_mod_add_left_eq,