src/Pure/proof_general.ML
changeset 15801 d2f5ca3c048d
parent 15629 4066f01f1beb
child 15964 f2074e12d1d4
--- a/src/Pure/proof_general.ML	Thu Apr 21 22:00:28 2005 +0200
+++ b/src/Pure/proof_general.ML	Thu Apr 21 22:02:06 2005 +0200
@@ -21,7 +21,6 @@
 
 signature PROOF_GENERAL =
 sig
-  val setup: (theory -> theory) list
   val update_thy_only: string -> unit
   val try_update_thy_only: string -> unit
   val inform_file_retracted: string -> unit
@@ -156,7 +155,11 @@
    ("bound", tagit bound_tag),
    ("var", var_or_skolem)];
 
-in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
+in
+
+val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
+
+end;
 
 
 (* assembling PGIP packets *)