src/HOL/Import/import_package.ML
changeset 18708 4b3dadb4fe33
parent 17657 2f5f595eb618
child 21590 ef7278f553eb
     1.1 --- a/src/HOL/Import/import_package.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Import/import_package.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  signature IMPORT_PACKAGE =
     1.5  sig
     1.6      val import_meth: Method.src -> Proof.context -> Proof.method
     1.7 -    val setup      : (theory -> theory) list
     1.8 +    val setup      : theory -> theory
     1.9      val debug      : bool ref
    1.10  end
    1.11  
    1.12 @@ -80,6 +80,6 @@
    1.13  			  Method.SIMPLE_METHOD (import_tac arg thy)
    1.14  		      end)
    1.15  
    1.16 -val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
    1.17 +val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
    1.18  end
    1.19