# HG changeset patch
# User wenzelm
# Date 1303475432 -7200
# Node ID 13b4b6ba359388fdb6b1d335166b35277846da4a
# Parent  6702c984bf5a6039633b123dd204ee6e8a047515
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;

diff -r 6702c984bf5a -r 13b4b6ba3593 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/FOL/FOL.thy	Fri Apr 22 14:30:32 2011 +0200
@@ -307,11 +307,11 @@
 use "simpdata.ML"
 
 simproc_setup defined_Ex ("EX x. P(x)") = {*
-  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
+  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
 *}
 
 simproc_setup defined_All ("ALL x. P(x)") = {*
-  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
+  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
 *}
 
 ML {*
diff -r 6702c984bf5a -r 13b4b6ba3593 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 22 14:30:32 2011 +0200
@@ -1213,11 +1213,11 @@
 setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
 
 simproc_setup defined_Ex ("EX x. P x") = {*
-  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
+  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
 *}
 
 simproc_setup defined_All ("ALL x. P x") = {*
-  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
+  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
 *}
 
 setup {*
diff -r 6702c984bf5a -r 13b4b6ba3593 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/HOL/Set.thy	Fri Apr 22 14:30:32 2011 +0200
@@ -77,13 +77,12 @@
 
 simproc_setup defined_Collect ("{x. P x & Q x}") = {*
   let
-    val Coll_perm_tac =
+    val Collect_perm_tac =
       rtac @{thm Collect_cong} 1 THEN
       rtac @{thm iffI} 1 THEN
       ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_Coll Coll_perm_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_Collect Collect_perm_tac ss o term_of
   end
 *}
 
@@ -333,8 +332,7 @@
     val unfold_bex_tac = unfold_tac @{thms Bex_def};
     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
   end
 *}
 
@@ -343,8 +341,7 @@
     val unfold_ball_tac = unfold_tac @{thms Ball_def};
     fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
   end
 *}
 
diff -r 6702c984bf5a -r 13b4b6ba3593 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/Provers/quantifier1.ML	Fri Apr 22 14:30:32 2011 +0200
@@ -66,11 +66,11 @@
 sig
   val prove_one_point_all_tac: tactic
   val prove_one_point_ex_tac: tactic
-  val rearrange_all: theory -> simpset -> term -> thm option
-  val rearrange_ex:  theory -> simpset -> term -> thm option
-  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
-  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
-  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
+  val rearrange_all: simpset -> term -> thm option
+  val rearrange_ex: simpset -> term -> thm option
+  val rearrange_ball: tactic -> simpset -> term -> thm option
+  val rearrange_bex: tactic -> simpset -> term -> thm option
+  val rearrange_Collect: tactic -> simpset -> term -> thm option
 end;
 
 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -112,14 +112,14 @@
         | exqu xs P = extract (null xs) xs P
   in exqu [] end;
 
-fun prove_conv tac thy tu =
-  let val ctxt = Proof_Context.init_global thy;
-      val eq_tu = Logic.mk_equals tu;
-      val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
-      val thm = Goal.prove ctxt' [] [] fixed_goal
-            (K (rtac iff_reflection 1 THEN tac));
-      val [gen_thm] = Variable.export ctxt' ctxt [thm];
-  in gen_thm end;
+fun prove_conv tac ss tu =
+  let
+    val ctxt = Simplifier.the_context ss;
+    val (goal, ctxt') =
+      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
+    val thm =
+      Goal.prove ctxt' [] [] goal (K (rtac iff_reflection 1 THEN tac));
+  in singleton (Variable.export ctxt' ctxt) thm end;
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
 
@@ -160,42 +160,42 @@
       val Q = if n=0 then P else renumber 0 n P
   in quant xs (qC $ Abs(x,T,Q)) end;
 
-fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
+fun rearrange_all ss (F as (all as Const(q,_)) $ Abs(x,T, P)) =
      (case extract_quant extract_imp q P of
         NONE => NONE
       | SOME(xs,eq,Q) =>
           let val R = quantify all x T xs (imp $ eq $ Q)
-          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
-  | rearrange_all _ _ _ = NONE;
+          in SOME (prove_conv prove_one_point_all_tac ss (F,R)) end)
+  | rearrange_all _ _ = NONE;
 
-fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
+fun rearrange_ball tac ss (F as Ball $ A $ Abs(x,T,P)) =
      (case extract_imp true [] P of
         NONE => NONE
       | SOME(xs,eq,Q) => if not(null xs) then NONE else
           let val R = imp $ eq $ Q
-          in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
-  | rearrange_ball _ _ _ _ = NONE;
+          in SOME (prove_conv tac ss (F,Ball $ A $ Abs(x,T,R))) end)
+  | rearrange_ball _ _ _ = NONE;
 
-fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
+fun rearrange_ex ss (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
      (case extract_quant extract_conj q P of
         NONE => NONE
       | SOME(xs,eq,Q) =>
           let val R = quantify ex x T xs (conj $ eq $ Q)
-          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
-  | rearrange_ex _ _ _ = NONE;
+          in SOME(prove_conv prove_one_point_ex_tac ss (F,R)) end)
+  | rearrange_ex _ _ = NONE;
 
-fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
+fun rearrange_bex tac ss (F as Bex $ A $ Abs(x,T,P)) =
      (case extract_conj true [] P of
         NONE => NONE
       | SOME(xs,eq,Q) => if not(null xs) then NONE else
-          SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
-  | rearrange_bex _ _ _ _ = NONE;
+          SOME(prove_conv tac ss (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
+  | rearrange_bex _ _ _ = NONE;
 
-fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) =
+fun rearrange_Collect tac ss (F as Coll $ Abs(x,T,P)) =
      (case extract_conj true [] P of
         NONE => NONE
       | SOME(_,eq,Q) =>
           let val R = Coll $ Abs(x,T, conj $ eq $ Q)
-          in SOME(prove_conv tac thy (F,R)) end);
+          in SOME(prove_conv tac ss (F,R)) end);
 
 end;
diff -r 6702c984bf5a -r 13b4b6ba3593 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/ZF/OrdQuant.thy	Fri Apr 22 14:30:32 2011 +0200
@@ -373,8 +373,7 @@
     val unfold_rex_tac = unfold_tac @{thms rex_def};
     fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_bex prove_rex_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss o term_of
   end
 *}
 
@@ -383,8 +382,7 @@
     val unfold_rall_tac = unfold_tac @{thms rall_def};
     fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_ball prove_rall_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss o term_of
   end
 *}
 
diff -r 6702c984bf5a -r 13b4b6ba3593 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/ZF/pair.thy	Fri Apr 22 14:30:32 2011 +0200
@@ -15,8 +15,7 @@
     val unfold_bex_tac = unfold_tac @{thms Bex_def};
     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
   end
 *}
 
@@ -25,8 +24,7 @@
     val unfold_ball_tac = unfold_tac @{thms Ball_def};
     fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
   in
-    fn _ => fn ss => fn ct =>
-      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
+    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
   end
 *}