src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Thu Apr 21 22:00:28 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 21 22:02:06 2005 +0200
@@ -6,6 +6,7 @@
 *)
 
 val show_structs = ref false;
+val thms_containing_limit = ref 40;
 
 signature PROOF_CONTEXT =
 sig
@@ -153,9 +154,7 @@
   val prems_limit: int ref
   val pretty_asms: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
-  val thms_containing_limit: int ref
   val print_thms_containing: context -> int option -> string list -> unit
-  val setup: (theory -> theory) list
 end;
 
 signature PRIVATE_PROOF_CONTEXT =
@@ -268,6 +267,7 @@
 end;
 
 structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
+val _ = Context.add_setup [ProofDataData.init];
 val print_proof_data = ProofDataData.print;
 
 
@@ -1464,8 +1464,6 @@
   in gen_distinct eq_fst (List.filter valid (FactIndex.find idx index)) end;
 
 
-val thms_containing_limit = ref 40;
-
 fun print_thms_containing ctxt opt_limit ss =
   let
     val prt_term = pretty_term ctxt;
@@ -1499,9 +1497,4 @@
   end;
 
 
-
-(** theory setup **)
-
-val setup = [ProofDataData.init];
-
 end;