New way of referring to Basis Library
authorpaulson
Sat Nov 01 13:01:07 1997 +0100 (1997-11-01)
changeset 4062fa2eb95b1b2d
parent 4061 5a2cc5752cb6
child 4063 0b19014b9155
New way of referring to Basis Library
TFL/sys.sml
TFL/tfl.sml
src/HOLCF/domain/theorems.ML
     1.1 --- a/TFL/sys.sml	Sat Nov 01 13:00:31 1997 +0100
     1.2 +++ b/TFL/sys.sml	Sat Nov 01 13:01:07 1997 +0100
     1.3 @@ -25,8 +25,8 @@
     1.4  
     1.5  use "usyntax.sml";
     1.6  use "thms.sml";
     1.7 -use"dcterm.sml"; 
     1.8 -use"rules.new.sml";
     1.9 +use "dcterm.sml"; 
    1.10 +use "rules.new.sml";
    1.11  use "thry.sml";
    1.12  
    1.13  
    1.14 @@ -34,4 +34,4 @@
    1.15   *      Link system and specialize for Isabelle 
    1.16   *---------------------------------------------------------------------------*)
    1.17  use "tfl.sml";
    1.18 -use"post.sml";
    1.19 +use "post.sml";
     2.1 --- a/TFL/tfl.sml	Sat Nov 01 13:00:31 1997 +0100
     2.2 +++ b/TFL/tfl.sml	Sat Nov 01 13:01:07 1997 +0100
     2.3 @@ -224,8 +224,9 @@
     2.4       case (ty_info ty_name)
     2.5       of None => mk_case_fail("Not a known datatype: "^ty_name)
     2.6        | Some{case_const,constructors} =>
     2.7 -        let val case_const_name = #1(dest_Const case_const)
     2.8 -            val nrows = List_.concat (map (expand constructors pty) rows)
     2.9 +        let open Basis_Library (*restore original List*)
    2.10 +	    val case_const_name = #1(dest_Const case_const)
    2.11 +            val nrows = List.concat (map (expand constructors pty) rows)
    2.12              val subproblems = divide(constructors, pty, range_ty, nrows)
    2.13              val groups      = map #group subproblems
    2.14              and new_formals = map #new_formals subproblems
    2.15 @@ -239,7 +240,7 @@
    2.16              val types = map type_of (case_functions@[u]) @ [range_ty]
    2.17              val case_const' = Const(case_const_name, list_mk_type types)
    2.18              val tree = list_comb(case_const', case_functions@[u])
    2.19 -            val pat_rect1 = List_.concat
    2.20 +            val pat_rect1 = List.concat
    2.21                                (ListPair.map mk_pat (constructors', pat_rect))
    2.22          in (pat_rect1,tree)
    2.23          end 
     3.1 --- a/src/HOLCF/domain/theorems.ML	Sat Nov 01 13:00:31 1997 +0100
     3.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Nov 01 13:01:07 1997 +0100
     3.3 @@ -267,8 +267,9 @@
     3.4          if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
     3.5          if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
     3.6                                          [eq1, eq2] end;
     3.7 +    open Basis_Library (*restore original List*)
     3.8      fun distincts []      = []
     3.9 -    |   distincts ((c,leqs)::cs) = List_.concat
    3.10 +    |   distincts ((c,leqs)::cs) = List.concat
    3.11  	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    3.12  		    distincts cs;
    3.13      in distincts (cons~~distincts_le) end;