1.1 --- a/src/HOLCF/HOLCF.ML	Fri Apr 01 23:44:41 2005 +0200
     1.2 +++ b/src/HOLCF/HOLCF.ML	Sat Apr 02 00:12:38 2005 +0200
     1.3 @@ -3,6 +3,11 @@
     1.4      Author:     Franz Regensburger
     1.5  *)
     1.6  
     1.7 +structure HOLCF =
     1.8 +struct
     1.9 +  val thy = the_context ();
    1.10 +end;
    1.11 +
    1.12  use"adm.ML";
    1.13  
    1.14  simpset_ref() := simpset() addSolver

     2.1 --- a/src/HOLCF/HOLCF.thy	Fri Apr 01 23:44:41 2005 +0200
     2.2 +++ b/src/HOLCF/HOLCF.thy	Sat Apr 02 00:12:38 2005 +0200
     2.3 @@ -5,4 +5,8 @@
     2.4  Top theory for HOLCF system.
     2.5  *)
     2.6  
     2.7 -HOLCF = Sprod + Ssum + Up + Lift + Discrete + One + Tr
     2.8 +theory HOLCF
     2.9 +imports Sprod Ssum Up Lift Discrete One Tr
    2.10 +begin
    2.11 +
    2.12 +end