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/Prolog/prolog.ML
changeset 32952 aeb1e44fbc19
parent 32740 9dd0a2f83429
child 35232 f588e1169c8b 
--- a/src/HOL/Prolog/prolog.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -106,7 +106,7 @@
         in Library.foldl (op APPEND) (no_tac, ptacs) st end;
 
 fun ptac ctxt prog = let
-  val proga = List.concat (map (atomizeD ctxt) prog)                   (* atomize the prog *)
+  val proga = maps (atomizeD ctxt) prog         (* atomize the prog *)
   in    (REPEAT_DETERM1 o FIRST' [
                 rtac TrueI,                     (* "True" *)
                 rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
isabelle