# HG changeset patch
# User paulson
# Date 878385667 -3600
# Node ID fa2eb95b1b2dfa8cf995b920d83a28456ea95983
# Parent  5a2cc5752cb660e362b50b2c1923b9a3b012335b
New way of referring to Basis Library

diff -r 5a2cc5752cb6 -r fa2eb95b1b2d TFL/sys.sml
--- 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";
diff -r 5a2cc5752cb6 -r fa2eb95b1b2d TFL/tfl.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 
diff -r 5a2cc5752cb6 -r fa2eb95b1b2d src/HOLCF/domain/theorems.ML
--- 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;