1.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Jan 12 14:32:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Jan 12 16:42:02 2014 +0100
     1.3 @@ -70,9 +70,8 @@
     1.4  (*Is this the best way to invoke the simplifier??*)
     1.5  fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
     1.6  
     1.7 -fun join_assums th =
     1.8 +fun join_assums ctxt th =
     1.9    let val thy = Thm.theory_of_thm th
    1.10 -      val ctxt = Proof_Context.init_global thy
    1.11        val tych = cterm_of thy
    1.12        val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
    1.13        val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
    1.14 @@ -101,7 +100,7 @@
    1.15                       if (id_thm th) then (So, Si, th::St) else
    1.16                       if (solved th) then (th::So, Si, St)
    1.17                       else (So, th::Si, St)) nested_tcs ([],[],[])
    1.18 -              val simplified' = map join_assums simplified
    1.19 +              val simplified' = map (join_assums ctxt) simplified
    1.20                val dummy = (Prim.trace_thms "solved =" solved;
    1.21                             Prim.trace_thms "simplified' =" simplified')
    1.22                val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
    1.23 @@ -189,9 +188,9 @@
    1.24  fun define_i strict ctxt congs wfs fid R eqs thy =
    1.25    let val {functional,pats} = Prim.mk_functional thy eqs
    1.26        val (thy, def) = Prim.wfrec_definition0 thy fid R functional
    1.27 -      val ctxt' = Proof_Context.transfer thy ctxt
    1.28 +      val ctxt = Proof_Context.transfer thy ctxt
    1.29        val (lhs, _) = Logic.dest_equals (prop_of def)
    1.30 -      val {induct, rules, tcs} = simplify_defn strict thy ctxt' congs wfs fid pats def
    1.31 +      val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def
    1.32        val rules' = 
    1.33            if strict then derive_init_eqs ctxt rules eqs
    1.34            else rules

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