--- a/TFL/sys.sml Sat Nov 01 13:00:31 1997 +0100
+++ b/TFL/sys.sml Sat Nov 01 13:01:07 1997 +0100
@@ -25,8 +25,8 @@
use "usyntax.sml";
use "thms.sml";
-use"dcterm.sml";
-use"rules.new.sml";
+use "dcterm.sml";
+use "rules.new.sml";
use "thry.sml";
@@ -34,4 +34,4 @@
* Link system and specialize for Isabelle
*---------------------------------------------------------------------------*)
use "tfl.sml";
-use"post.sml";
+use "post.sml";
--- a/TFL/tfl.sml Sat Nov 01 13:00:31 1997 +0100
+++ b/TFL/tfl.sml Sat Nov 01 13:01:07 1997 +0100
@@ -224,8 +224,9 @@
case (ty_info ty_name)
of None => mk_case_fail("Not a known datatype: "^ty_name)
| Some{case_const,constructors} =>
- let val case_const_name = #1(dest_Const case_const)
- val nrows = List_.concat (map (expand constructors pty) rows)
+ let open Basis_Library (*restore original List*)
+ val case_const_name = #1(dest_Const case_const)
+ val nrows = List.concat (map (expand constructors pty) rows)
val subproblems = divide(constructors, pty, range_ty, nrows)
val groups = map #group subproblems
and new_formals = map #new_formals subproblems
@@ -239,7 +240,7 @@
val types = map type_of (case_functions@[u]) @ [range_ty]
val case_const' = Const(case_const_name, list_mk_type types)
val tree = list_comb(case_const', case_functions@[u])
- val pat_rect1 = List_.concat
+ val pat_rect1 = List.concat
(ListPair.map mk_pat (constructors', pat_rect))
in (pat_rect1,tree)
end
--- a/src/HOLCF/domain/theorems.ML Sat Nov 01 13:00:31 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Sat Nov 01 13:01:07 1997 +0100
@@ -267,8 +267,9 @@
if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
[eq1, eq2] end;
+ open Basis_Library (*restore original List*)
fun distincts [] = []
- | distincts ((c,leqs)::cs) = List_.concat
+ | distincts ((c,leqs)::cs) = List.concat
(ListPair.map (distinct c) ((map #1 cs),leqs)) @
distincts cs;
in distincts (cons~~distincts_le) end;