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.
src/Provers/preorder.ML
changeset 81541 5335b1ca6233
parent 81516 31b05aef022d 
--- a/src/Provers/preorder.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/Provers/preorder.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -555,7 +555,7 @@
 fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt;
-  val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
+  val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
@@ -578,7 +578,7 @@
 fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt
-  val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
+  val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
isabelle