src/HOL/Tools/datatype_prop.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 17521 0f1c48de39f5
--- a/src/HOL/Tools/datatype_prop.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -80,7 +80,7 @@
              (map HOLogic.mk_eq (frees ~~ frees')))))::injs
         end;
 
-  in map (fn (d, T) => Library.foldr (make_inj T) (#3 (snd d), []))
+  in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
     ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
   end;
 
@@ -182,7 +182,7 @@
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = Library.foldr add_typ_tfree_names (recTs, []);
+    val used = foldr add_typ_tfree_names [] recTs;
 
     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
 
@@ -232,7 +232,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = Library.foldr add_typ_tfree_names (recTs, []);
+    val used = foldr add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (variant used "'t", HOLogic.typeS);
 
@@ -317,7 +317,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used' = Library.foldr add_typ_tfree_names (recTs, []);
+    val used' = foldr add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
@@ -334,13 +334,13 @@
             val eqn = HOLogic.mk_eq (Free ("x", T),
               list_comb (Const (cname, Ts ---> T), frees));
             val P' = P $ list_comb (f, frees)
-          in ((Library.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
-                (frees, HOLogic.imp $ eqn $ P'))::t1s,
-              (Library.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
-                (frees, HOLogic.conj $ eqn $ (HOLogic.Not $ P')))::t2s)
+          in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
+                (HOLogic.imp $ eqn $ P') frees)::t1s,
+              (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
+                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
           end;
 
-        val (t1s, t2s) = Library.foldr process_constr (constrs ~~ fs, ([], []));
+        val (t1s, t2s) = foldr process_constr ([], []) (constrs ~~ fs);
         val lhs = P $ (comb_t $ Free ("x", T))
       in
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
@@ -475,9 +475,9 @@
         val tnames = variantlist (make_tnames Ts, ["v"]);
         val frees = tnames ~~ Ts
       in
-        Library.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
-          (frees, HOLogic.mk_eq (Free ("v", T),
-            list_comb (Const (cname, Ts ---> T), map Free frees)))
+        foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
+          (HOLogic.mk_eq (Free ("v", T),
+            list_comb (Const (cname, Ts ---> T), map Free frees))) frees
       end
 
   in map (fn ((_, (_, _, constrs)), T) =>