src/HOL/Tools/TFL/post.ML

 users specification of the recursive function. *)
 local
   fun get_related_thms i = 
       map_filter ((fn (r,x) => if x = i then SOME r else NONE));
 
-  fun solve_eq (th, [], i) =  error "derive_init_eqs: missing rules"
-    | solve_eq (th, [a], i) = [(a, i)]
-    | solve_eq (th, splitths, i) =
+  fun solve_eq _ (th, [], i) =  error "derive_init_eqs: missing rules"
+    | solve_eq _ (th, [a], i) = [(a, i)]
+    | solve_eq ctxt (th, splitths, i) =
       (writeln "Proving unsplit equation...";
       [((Drule.export_without_context o Object_Logic.rulify_no_asm)
-          (CaseSplit.splitto splitths th), i)])
+          (CaseSplit.splitto ctxt splitths th), i)])
       handle ERROR s => 
              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
 in
-fun derive_init_eqs thy rules eqs =
-  map (Thm.trivial o Thm.cterm_of thy o HOLogic.mk_Trueprop) eqs
-  |> map_index (fn (i, e) => solve_eq (e, (get_related_thms i rules), i))
+fun derive_init_eqs ctxt rules eqs =
+  map (Thm.trivial o Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop) eqs
+  |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
   |> flat;
 end;
 
 
 (*---------------------------------------------------------------------------

       val (thy, def) = Prim.wfrec_definition0 thy fid R functional
       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 rules' = 
-          if strict then derive_init_eqs thy rules eqs
+          if strict then derive_init_eqs ctxt rules eqs
           else rules
   in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end;
 
 fun define strict ctxt congs wfs fid R seqs thy =
   define_i strict ctxt congs wfs fid