# HG changeset patch
# User wenzelm
# Date 1152356081 -7200
# Node ID 7f32ce6354d6e55dc50b10be2aa0e078c73f9a35
# Parent  3d4ff822d0b3840be87ebab8dd9d93699a4891bc
presburger_ss: proper context;

diff -r 3d4ff822d0b3 -r 7f32ce6354d6 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Sat Jul 08 12:54:40 2006 +0200
+++ b/src/HOL/Integ/presburger.ML	Sat Jul 08 12:54:41 2006 +0200
@@ -30,7 +30,7 @@
 (*-----------------------------------------------------------------*)
 
 
-val presburger_ss = simpset_of (theory "Presburger");
+val presburger_ss = simpset ();
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
diff -r 3d4ff822d0b3 -r 7f32ce6354d6 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Sat Jul 08 12:54:40 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Jul 08 12:54:41 2006 +0200
@@ -30,7 +30,7 @@
 (*-----------------------------------------------------------------*)
 
 
-val presburger_ss = simpset_of (theory "Presburger");
+val presburger_ss = simpset ();
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
  "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",