structure BasisLibrary;
authorwenzelm
Wed Nov 12 16:27:13 1997 +0100 (1997-11-12)
changeset 4221ed0f67fb458b
parent 4220 3cc85acd9ba8
child 4222 d7573d6d0513
structure BasisLibrary;
TFL/tfl.sml
src/HOLCF/domain/theorems.ML
     1.1 --- a/TFL/tfl.sml	Wed Nov 12 16:26:05 1997 +0100
     1.2 +++ b/TFL/tfl.sml	Wed Nov 12 16:27:13 1997 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4       case (ty_info ty_name)
     1.5       of None => mk_case_fail("Not a known datatype: "^ty_name)
     1.6        | Some{case_const,constructors} =>
     1.7 -        let open Basis_Library (*restore original List*)
     1.8 +        let open BasisLibrary (*restore original List*)
     1.9  	    val case_const_name = #1(dest_Const case_const)
    1.10              val nrows = List.concat (map (expand constructors pty) rows)
    1.11              val subproblems = divide(constructors, pty, range_ty, nrows)
     2.1 --- a/src/HOLCF/domain/theorems.ML	Wed Nov 12 16:26:05 1997 +0100
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Nov 12 16:27:13 1997 +0100
     2.3 @@ -267,7 +267,7 @@
     2.4          if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
     2.5          if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
     2.6                                          [eq1, eq2] end;
     2.7 -    open Basis_Library (*restore original List*)
     2.8 +    open BasisLibrary (*restore original List*)
     2.9      fun distincts []      = []
    2.10      |   distincts ((c,leqs)::cs) = List.concat
    2.11  	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @