# HG changeset patch
# User wenzelm
# Date 1152356080 -7200
# Node ID 3d4ff822d0b3840be87ebab8dd9d93699a4891bc
# Parent  859e7129961bd1b082b0bdfe0e6f2e75f4ded517
presburger_ss: proper context;
Goal.prove: context;

diff -r 859e7129961b -r 3d4ff822d0b3 src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Sat Jul 08 12:54:39 2006 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Sat Jul 08 12:54:40 2006 +0200
@@ -30,13 +30,9 @@
 struct
 open CooperDec;
 
-(*
-val presburger_ss = simpset_of (theory "Presburger")
-  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
-*)
+val presburger_ss = simpset ()
+  addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
 
-val presburger_ss = simpset_of (theory "Presburger")
-  addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
 
 (*Theorems that will be used later for the proofgeneration*)
@@ -44,7 +40,7 @@
 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
 val unity_coeff_ex = thm "unity_coeff_ex";
 
-(* Thorems for proving the adjustment of the coeffitients*)
+(* Theorems for proving the adjustment of the coefficients*)
 
 val ac_lt_eq =  thm "ac_lt_eq";
 val ac_eq_eq = thm "ac_eq_eq";
@@ -194,7 +190,7 @@
   (essentially) that are only to make at runtime.*)
 (* ------------------------------------------------------------------------- *)
 fun prove_elementar thy s fm2 =
-  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
+  Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
   (case s of
   (*"ss" like simplification with simpset*)
   "ss" =>
diff -r 859e7129961b -r 3d4ff822d0b3 src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jul 08 12:54:39 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jul 08 12:54:40 2006 +0200
@@ -30,13 +30,9 @@
 struct
 open CooperDec;
 
-(*
-val presburger_ss = simpset_of (theory "Presburger")
-  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
-*)
+val presburger_ss = simpset ()
+  addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
 
-val presburger_ss = simpset_of (theory "Presburger")
-  addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
 
 (*Theorems that will be used later for the proofgeneration*)
@@ -44,7 +40,7 @@
 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
 val unity_coeff_ex = thm "unity_coeff_ex";
 
-(* Thorems for proving the adjustment of the coeffitients*)
+(* Theorems for proving the adjustment of the coefficients*)
 
 val ac_lt_eq =  thm "ac_lt_eq";
 val ac_eq_eq = thm "ac_eq_eq";
@@ -194,7 +190,7 @@
   (essentially) that are only to make at runtime.*)
 (* ------------------------------------------------------------------------- *)
 fun prove_elementar thy s fm2 =
-  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
+  Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
   (case s of
   (*"ss" like simplification with simpset*)
   "ss" =>