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/Pure/Isar/element.ML
changeset 52789 44fd3add1348
parent 52788 da1fdbfebd39
child 54740 91f54d386680 
--- a/src/Pure/Isar/element.ML	Tue Jul 30 15:09:25 2013 +0200
+++ b/src/Pure/Isar/element.ML	Tue Jul 30 15:20:38 2013 +0200
@@ -395,7 +395,7 @@
    {binding = [],
     typ = [instT_type env],
     term = [instT_term env],
-    fact = [map (fn th => instT_thm thy env th)]};
+    fact = [map (instT_thm thy env)]};
 
 
 (* instantiate types and terms *)
@@ -438,7 +438,7 @@
    {binding = [],
     typ = [instT_type envT],
     term = [inst_term (envT, env)],
-    fact = [map (fn th => inst_thm thy (envT, env) th)]};
+    fact = [map (inst_thm thy (envT, env))]};
 
 
 (* satisfy hypotheses *)
isabelle