clarified context;

--- a/src/HOL/Tools/TFL/post.ML	Sun Jan 12 14:32:22 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sun Jan 12 16:42:02 2014 +0100
@@ -70,9 +70,8 @@
 (*Is this the best way to invoke the simplifier??*)
 fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
 
-fun join_assums th =
+fun join_assums ctxt th =
   let val thy = Thm.theory_of_thm th
-      val ctxt = Proof_Context.init_global thy
       val tych = cterm_of thy
       val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
       val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
@@ -101,7 +100,7 @@
                      if (id_thm th) then (So, Si, th::St) else
                      if (solved th) then (th::So, Si, St)
                      else (So, th::Si, St)) nested_tcs ([],[],[])
-              val simplified' = map join_assums simplified
+              val simplified' = map (join_assums ctxt) simplified
               val dummy = (Prim.trace_thms "solved =" solved;
                            Prim.trace_thms "simplified' =" simplified')
               val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
@@ -189,9 +188,9 @@
 fun define_i strict ctxt congs wfs fid R eqs thy =
   let val {functional,pats} = Prim.mk_functional thy eqs
       val (thy, def) = Prim.wfrec_definition0 thy fid R functional
-      val ctxt' = Proof_Context.transfer thy ctxt
+      val ctxt = Proof_Context.transfer thy ctxt
       val (lhs, _) = Logic.dest_equals (prop_of def)
-      val {induct, rules, tcs} = simplify_defn strict thy ctxt' congs wfs fid pats def
+      val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def
       val rules' = 
           if strict then derive_init_eqs ctxt rules eqs
           else rules

--- a/src/HOL/Tools/TFL/tfl.ML	Sun Jan 12 14:32:22 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Sun Jan 12 16:42:02 2014 +0100
@@ -432,7 +432,7 @@
        not simplified. Otherwise large examples (Red-Black trees) are too
        slow.*)
      val case_simpset =
-       put_simpset HOL_basic_ss (Proof_Context.init_global theory)
+       put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #weak_case_cong o snd)
               (Symtab.dest (Datatype.get_all theory))