Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thm.eta_long_conversion;
authorwenzelm
Mon, 25 Jun 2007 00:36:37 +0200
changeset 23488 342029af73d1
parent 23487 c48defc2b28c
child 23489 6c2156c478f6
Thm.eta_long_conversion;
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Qelim/presburger.ML	Mon Jun 25 00:36:36 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Mon Jun 25 00:36:37 2007 +0200
@@ -148,7 +148,7 @@
    NONE => no_tac st
  | SOME p => 
    let
-    val eq = (eta_conv (ProofContext.theory_of ctxt) then_conv Thm.beta_conversion true) p
+    val eq = (Thm.eta_long_conversion then_conv Thm.beta_conversion true) p
     val p' = Thm.rhs_of eq
     val th = implies_intr p' (equal_elim (symmetric eq) (assume p'))
    in rtac th i st
isabelle