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.
tuned;
authorwenzelm
Thu, 26 Aug 2010 16:56:45 +0200
changeset 38760 6f285436e3d6
parent 38759 37a9092de102
child 38761 b32975d3db3e
tuned;
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Aug 26 16:34:10 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Aug 26 16:56:45 2010 +0200
@@ -21,8 +21,7 @@
 structure Fun_Pred = Theory_Data
 (
   type T = (term * term) Item_Net.T;
-  val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
-    (single o fst);
+  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   val extend = I;
   val merge = Item_Net.merge;
 )
isabelle