# HG changeset patch
# User wenzelm
# Date 1236280622 -3600
# Node ID b28caca9157f92f556df89d040a0afc6c0f6e46e
# Parent  a32700e45ab30ec6d4d805d52e3d1952f19abcc6
removed spurious occurrences of old rep_ss;

diff -r a32700e45ab3 -r b28caca9157f src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Mar 05 19:48:02 2009 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Mar 05 20:17:02 2009 +0100
@@ -352,14 +352,14 @@
   | distinctTree_tac _ _ _ = no_tac;
 
 fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
-     (fn ss => case #context (#1 (rep_ss ss)) of
+     (fn ss => case try Simplifier.the_context ss of
                  SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
                 | NONE => fn i => no_tac)
 
 fun distinct_simproc names =
   Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
     (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
-        case #context (#1 (rep_ss ss)) of
+        case try Simplifier.the_context ss of
         SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
                       (get_fst_success (neq_x_y ctxt x y) names)
        | NONE => NONE
diff -r a32700e45ab3 -r b28caca9157f src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Mar 05 19:48:02 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Thu Mar 05 20:17:02 2009 +0100
@@ -146,7 +146,7 @@
           
           val ct = cterm_of thy 
                     (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
-          val ctxt = the (#context (#1 (rep_ss ss)));
+          val ctxt = Simplifier.the_context ss;
           val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
           val ss' = Simplifier.context 
                      (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss;
@@ -241,7 +241,7 @@
                       end
                | mk_updterm _ t = init_seed t;
 
-	     val ctxt = the (#context (#1 (rep_ss ss))) |>
+	     val ctxt = Simplifier.the_context ss |>
                         Config.map MetaSimplifier.simp_depth_limit (K 100);
              val ss1 = Simplifier.context ctxt ss';
              val ss2 = Simplifier.context ctxt 
diff -r a32700e45ab3 -r b28caca9157f src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Mar 05 19:48:02 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 05 20:17:02 2009 +0100
@@ -236,14 +236,14 @@
   | distinctTree_tac _ _ = no_tac;
 
 val distinctNameSolver = mk_solver' "distinctNameSolver"
-     (fn ss => case #context (#1 (rep_ss ss)) of
+     (fn ss => case try Simplifier.the_context ss of
                  SOME ctxt => SUBGOAL (distinctTree_tac ctxt)
                 | NONE => fn i => no_tac)
 
 val distinct_simproc =
   Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
     (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
-        (case #context (#1 (rep_ss ss)) of
+        (case try Simplifier.the_context ss of
           SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
                        (neq_x_y ctxt x y)
         | NONE => NONE)