src/HOL/Tools/TFL/rules.ML

   val tracing: bool Unsynchronized.ref
   val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
                              -> thm -> thm * term list
   val RIGHT_ASSOC: Proof.context -> thm -> thm
 
-  val prove: bool -> cterm * tactic -> thm
+  val prove: Proof.context -> bool -> term * tactic -> thm
 end;
 
 structure Rules: RULES =
 struct
 

  in
  (th2, filter_out restricted (!tc_list))
  end;
 
 
-fun prove strict (ptm, tac) =
+fun prove ctxt strict (t, tac) =
   let
-    val thy = Thm.theory_of_cterm ptm;
-    val t = Thm.term_of ptm;
-    val ctxt = Proof_Context.init_global thy |> Variable.auto_fixes t;
+    val ctxt' = Variable.auto_fixes t ctxt;
   in
-    if strict then Goal.prove ctxt [] [] t (K tac)
-    else Goal.prove ctxt [] [] t (K tac)
+    if strict
+    then Goal.prove ctxt' [] [] t (K tac)
+    else Goal.prove ctxt' [] [] t (K tac)
       handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
   end;
 
 end;