src/HOL/Tools/Function/function_lib.ML

   val rename_bound: string -> term -> term
   val mk_forall_rename: (string * term) -> term -> term
   val forall_intr_rename: (string * cterm) -> thm -> thm
 
   datatype proof_attempt = Solved of thm | Stuck of thm | Fail
-  val try_proof: cterm -> tactic -> proof_attempt
+  val try_proof: Proof.context -> cterm -> tactic -> proof_attempt
 
   val dest_binop_list: string -> term -> term list
   val regroup_conv: Proof.context -> string -> string -> thm list -> int list -> conv
   val regroup_union_conv: Proof.context -> int list -> conv
 

   in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end
 
 
 datatype proof_attempt = Solved of thm | Stuck of thm | Fail
 
-fun try_proof cgoal tac =
-  case SINGLE tac (Goal.init cgoal) of
+fun try_proof ctxt cgoal tac =
+  (case SINGLE tac (Goal.init cgoal) of
     NONE => Fail
   | SOME st =>
-    if Thm.no_prems st
-    then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
-    else Stuck st
+      if Thm.no_prems st
+      then Solved (Goal.finish ctxt st)
+      else Stuck st)
 
 
 fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
   if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
   | dest_binop_list _ t = [ t ]