Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/rules.ML
changeset 21370 d9dd7b4e5e69
parent 20951 868120282837
child 21858 05f57309170c 
--- a/TFL/rules.ML	Tue Nov 14 22:17:00 2006 +0100
+++ b/TFL/rules.ML	Tue Nov 14 22:17:01 2006 +0100
@@ -816,7 +816,7 @@
 fun prove strict (ptm, tac) =
   let
     val {thy, t, ...} = Thm.rep_cterm ptm;
-    val ctxt = ProofContext.init thy |> Variable.fix_frees t;
+    val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
   in
     if strict then Goal.prove ctxt [] [] t (K tac)
     else Goal.prove ctxt [] [] t (K tac)
isabelle