src/HOL/Integ/presburger.ML
changeset 20053 7f32ce6354d6
parent 19277 f7602e74d948
child 20194 c9dbce9a23a1
--- 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",