# HG changeset patch
# User wenzelm
# Date 1414592117 -3600
# Node ID 513268cb217834fa5bdeb4d4d8b0776b4f6bec53
# Parent  90a5e981af3ed8483fb46e7264168f522c7da4c6
modernized setup;

diff -r 90a5e981af3e -r 513268cb2178 src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Wed Oct 29 15:07:53 2014 +0100
+++ b/src/HOL/Predicate_Compile.thy	Wed Oct 29 15:15:17 2014 +0100
@@ -21,7 +21,6 @@
 ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
 ML_file "Tools/Predicate_Compile/predicate_compile.ML"
 
-setup Predicate_Compile.setup
 
 subsection {* Set membership as a generator predicate *}
 
diff -r 90a5e981af3e -r 513268cb2178 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Oct 29 15:07:53 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Oct 29 15:15:17 2014 +0100
@@ -27,7 +27,7 @@
     needs_random : mode list
   };
 
-  structure PredData : THEORY_DATA
+  structure PredData : THEORY_DATA  (* FIXME keep data private *)
   
   (* queries *)
   val defined_functions : compilation -> Proof.context -> string -> bool
diff -r 90a5e981af3e -r 513268cb2178 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Oct 29 15:07:53 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Oct 29 15:15:17 2014 +0100
@@ -7,7 +7,6 @@
 
 signature PREDICATE_COMPILE =
 sig
-  val setup : theory -> theory
   val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory
   val present_graph : bool Unsynchronized.ref
   val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
@@ -213,8 +212,6 @@
     else Predicate_Compile_Core.code_pred_cmd options raw_const lthy
   end
 
-val setup = Predicate_Compile_Core.setup
-
 
 (* Parser for mode annotations *)
 
diff -r 90a5e981af3e -r 513268cb2178 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 29 15:07:53 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 29 15:15:17 2014 +0100
@@ -12,7 +12,6 @@
   type compilation = Predicate_Compile_Aux.compilation
   type compilation_funs = Predicate_Compile_Aux.compilation_funs
 
-  val setup : theory -> theory
   val code_pred : options -> string -> Proof.context -> Proof.state
   val code_pred_cmd : options -> string -> Proof.context -> Proof.state
   val values_cmd : string list -> mode option list option ->
@@ -1615,10 +1614,11 @@
 val values_timeout =
   Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
 
-val setup =
-  PredData.put (Graph.empty) #>
-  Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
-    "adding alternative introduction rules for code generation of inductive predicates"
+val _ =
+  Theory.setup
+   (PredData.put (Graph.empty) #>
+    Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
+      "adding alternative introduction rules for code generation of inductive predicates")
 
 fun qualified_binding a =
   Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));