# HG changeset patch
# User wenzelm
# Date 1433173485 -7200
# Node ID edac62cd7bdeefc26c4791620a3223512d67de18
# Parent  63f25a1adcfc01e4c46dfc9ea8438205a34654cf
clarified context;

diff -r 63f25a1adcfc -r edac62cd7bde src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Mon Jun 01 17:08:47 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon Jun 01 17:44:45 2015 +0200
@@ -51,7 +51,7 @@
                              -> 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 =
@@ -792,14 +792,13 @@
  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;
 
diff -r 63f25a1adcfc -r edac62cd7bde src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon Jun 01 17:08:47 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Jun 01 17:44:45 2015 +0200
@@ -914,15 +914,13 @@
 fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
 let val ctxt = Proof_Context.init_global theory;
     val tych = Thry.typecheck theory;
-    val prove = Rules.prove strict;
 
    (*---------------------------------------------------------------------
     * Attempt to eliminate WF condition. It's the only assumption of rules
     *---------------------------------------------------------------------*)
    val (rules1,induction1)  =
-       let val thm = prove(tych(HOLogic.mk_Trueprop
-                                  (hd(#1(Rules.dest_thm rules)))),
-                             wf_tac)
+       let val thm =
+        Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
        in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
        end handle Utils.ERR _ => (rules,induction);
 
@@ -944,7 +942,7 @@
        elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
        handle Utils.ERR _ =>
         (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
-                  (prove(tych(HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq))),
+                  (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
                            terminator)))
                  (r,ind)
          handle Utils.ERR _ =>
@@ -972,7 +970,7 @@
        (Rules.MATCH_MP Thms.eqT tc_eq
         handle Utils.ERR _ =>
           (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
-                      (prove(tych(HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq))),
+                      (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
                                terminator))
             handle Utils.ERR _ => tc_eq))
       end