diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/sys.sml --- a/TFL/sys.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/sys.sml Tue Jun 03 11:08:08 1997 +0200 @@ -12,20 +12,11 @@ (* Establish a base of common and/or helpful functions. *) use "utils.sig"; -(* Get the specifications - these are independent of any system *) use "usyntax.sig"; use "rules.sig"; use "thry.sig"; use "thms.sig"; use "tfl.sig"; - -(*---------------------------------------------------------------------------- - * Load the TFL functor - this is defined totally in terms of the - * above interfaces. - *---------------------------------------------------------------------------*) - -use "tfl.sml"; - use "utils.sml"; (*---------------------------------------------------------------------------- @@ -42,8 +33,5 @@ (*---------------------------------------------------------------------------- * Link system and specialize for Isabelle *---------------------------------------------------------------------------*) -structure Prim = TFL(structure Rules = FastRules - structure Thms = Thms - structure Thry = Thry); - +use "tfl.sml"; use"post.sml";