--- a/src/Pure/Tools/compute.ML Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Tools/compute.ML Thu Apr 27 15:06:35 2006 +0200
@@ -24,7 +24,7 @@
exception Make of string;
-fun is_mono_typ (Type (_, list)) = List.all is_mono_typ list
+fun is_mono_typ (Type (_, list)) = forall is_mono_typ list
| is_mono_typ _ = false
fun is_mono_term (Const (_, t)) = is_mono_typ t
@@ -247,9 +247,8 @@
let
val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)
fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th'])
- fun app f l = List.concat (map f l)
in
- basic_make thy (app mk (app mk_eq_True ths))
+ basic_make thy (maps mk (maps mk_eq_True ths))
end
fun compute (Computer r) naming ct =