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/post.ML
changeset 16287 7a03b4b4df67
parent 15574 b1d1b5bfc464
child 16852 b950180e243d 
--- a/TFL/post.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/TFL/post.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -45,7 +45,7 @@
  * have a tactic directly applied to them.
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
-    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
+    map (Type.freeze o HOLogic.dest_Trueprop)
       (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------
isabelle