src/Pure/Tools/am_compiler.ML
changeset 19482 9f11af8f7ef9
parent 17795 5b18c3343028
child 20668 00521d5e1838
--- a/src/Pure/Tools/am_compiler.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Tools/am_compiler.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -113,7 +113,7 @@
   | remove_dups [] = []
 
 fun constants_of PVar = []
-  | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
+  | constants_of (PConst (c, ps)) = c :: maps constants_of ps
 
 fun constants_of_term (Var _) = []
   | constants_of_term (Abs m) = constants_of_term m
@@ -133,7 +133,7 @@
 		"structure "^name^" = struct",
 		"",
 		"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
-	val constants = remove_dups (List.concat (map (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog))
+	val constants = remove_dups (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
 	val _ = map (fn x => write (" | c"^(str x))) constants
 	val _ = writelist [
 		"",