src/ZF/Tools/typechk.ML
changeset 18708 4b3dadb4fe33
parent 17886 9a4aea3a9ae1
child 18736 541d04c79e12
     1.1 --- a/src/ZF/Tools/typechk.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/ZF/Tools/typechk.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  signature TYPE_CHECK =
     1.5  sig
     1.6    include BASIC_TYPE_CHECK
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure TypeCheck: TYPE_CHECK =
    1.12 @@ -210,10 +210,11 @@
    1.13  (** theory setup **)
    1.14  
    1.15  val setup =
    1.16 - [TypecheckingData.init, LocalTypecheckingData.init,
    1.17 -  fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy),
    1.18 -  Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
    1.19 -  Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
    1.20 + (TypecheckingData.init #>
    1.21 +  LocalTypecheckingData.init #>
    1.22 +  (fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy)) #>
    1.23 +  Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")] #>
    1.24 +  Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]);
    1.25  
    1.26  
    1.27  (** outer syntax **)