--- a/src/HOL/HOL.thy Sat Aug 16 20:27:51 2014 +0200
+++ b/src/HOL/HOL.thy Sat Aug 16 20:46:59 2014 +0200
@@ -1965,29 +1965,12 @@
subsection {* Preprocessing for the predicate compiler *}
-ML {*
-structure Predicate_Compile_Alternative_Defs = Named_Thms
-(
- val name = @{binding code_pred_def}
- val description = "alternative definitions of constants for the Predicate Compiler"
-)
-structure Predicate_Compile_Inline_Defs = Named_Thms
-(
- val name = @{binding code_pred_inline}
- val description = "inlining definitions for the Predicate Compiler"
-)
-structure Predicate_Compile_Simps = Named_Thms
-(
- val name = @{binding code_pred_simp}
- val description = "simplification rules for the optimisations in the Predicate Compiler"
-)
-*}
-
-setup {*
- Predicate_Compile_Alternative_Defs.setup
- #> Predicate_Compile_Inline_Defs.setup
- #> Predicate_Compile_Simps.setup
-*}
+named_theorems code_pred_def
+ "alternative definitions of constants for the Predicate Compiler"
+named_theorems code_pred_inline
+ "inlining definitions for the Predicate Compiler"
+named_theorems code_pred_simp
+ "simplification rules for the optimisations in the Predicate Compiler"
subsection {* Legacy tactics and ML bindings *}
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Aug 16 20:27:51 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Aug 16 20:46:59 2014 +0200
@@ -1047,7 +1047,8 @@
val thy = Proof_Context.theory_of ctxt
val ((((full_constname, constT), vs'), intro), thy1) =
Predicate_Compile_Aux.define_quickcheck_predicate t' thy
- val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
+ val thy2 =
+ Context.theory_map (Named_Theorems.add_thm @{named_theorems code_pred_def} intro) thy1
val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
val ctxt' = Proof_Context.init_global thy3
val _ = tracing "Generating prolog program..."
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Aug 16 20:27:51 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Aug 16 20:46:59 2014 +0200
@@ -1042,7 +1042,7 @@
let
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val process =
- rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
+ rewrite_rule ctxt (Named_Theorems.get ctxt @{named_theorems code_pred_simp})
fun process_False intro_t =
if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
then NONE else SOME intro_t
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 16 20:27:51 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 16 20:46:59 2014 +0200
@@ -161,8 +161,8 @@
fun inline_equations thy th =
let
val ctxt = Proof_Context.init_global thy
- val inline_defs = Predicate_Compile_Inline_Defs.get ctxt
- val th' = (Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs)) th
+ val inline_defs = Named_Theorems.get ctxt @{named_theorems code_pred_inline}
+ val th' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs) th
(*val _ = print_step options
("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
@@ -208,12 +208,12 @@
NONE
fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
val spec =
- (case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
+ (case filter_defs (Named_Theorems.get ctxt @{named_theorems code_pred_def}) of
[] =>
(case Spec_Rules.retrieve ctxt t of
[] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
| ((_, (_, ths)) :: _) => filter_defs ths)
- | ths => rev ths)
+ | ths => ths)
val _ =
if show_intermediate_results options then
tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Aug 16 20:27:51 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Aug 16 20:46:59 2014 +0200
@@ -231,7 +231,8 @@
val thy = Proof_Context.theory_of ctxt
val ((((full_constname, constT), vs'), intro), thy1) =
Predicate_Compile_Aux.define_quickcheck_predicate t' thy
- val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
+ val thy2 =
+ Context.theory_map (Named_Theorems.add_thm @{named_theorems code_pred_def} intro) thy1
val (thy3, _) = cpu_time "predicate preprocessing"
(fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
val (thy4, _) = cpu_time "random_dseq core compilation"