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/eqsubst.ML
changeset 21708 45e7491bea47
parent 21588 cd0dc678a205
child 21879 a3efbae45735 
--- a/src/Provers/eqsubst.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Provers/eqsubst.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -415,7 +415,7 @@
       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
       val preelimrule =
           (RWInst.rw m rule pth)
-            |> (Seq.hd o Tactic.prune_params_tac)
+            |> (Seq.hd o prune_params_tac)
             |> Thm.permute_prems 0 ~1 (* put old asm first *)
             |> IsaND.unfix_frees cfvs (* unfix any global params *)
             |> RWInst.beta_eta_contract; (* normal form *)
isabelle