--- 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 *}
--- 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
--- 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 *)
--- 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));