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/HOL/Tools/ATP/atp_util.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59632 5980e75a204e 
--- a/src/HOL/Tools/ATP/atp_util.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -353,7 +353,7 @@
 fun abs_extensionalize_term ctxt t =
   if exists_Const is_fun_equality t then
     let val thy = Proof_Context.theory_of ctxt in
-      t |> Thm.cterm_of thy |> Meson.abs_extensionalize_conv ctxt
+      t |> Thm.global_cterm_of thy |> Meson.abs_extensionalize_conv ctxt
         |> Thm.prop_of |> Logic.dest_equals |> snd
     end
   else
isabelle