tactic and the rest eliminated, just the theory....

--- a/src/HOL/ex/Reflected_Presburger.thy	Wed Sep 14 21:35:46 2005 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Sep 14 21:44:27 2005 +0200
@@ -4,7 +4,7 @@
 
 theory Reflected_Presburger
 imports Main
-uses ("rcooper.ML") ("rpresbtac.ML")
+(* uses ("rcooper.ML") ("rpresbtac.ML") *)
 begin
 
 (* Shadow syntax for integer terms *)
@@ -5717,10 +5717,9 @@
 
 (*
 generate_code ("presburger.ML") test = "pa"
-*)
 use "rcooper.ML"
 oracle rpresburger_oracle ("term") = RCooper.rpresburger_oracle
 use "rpresbtac.ML"
 setup RPresburger.setup
-
+*)
 end