# HG changeset patch
# User wenzelm
# Date 1408214819 -7200
# Node ID 0284a7d083be34ea4655888db434e449929d6f1b
# Parent  10b2f60b70f0b65e9e12de500828813a2a2dd5d1
updated to named_theorems;

diff -r 10b2f60b70f0 -r 0284a7d083be src/HOL/HOL.thy
--- 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 *}
diff -r 10b2f60b70f0 -r 0284a7d083be src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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..."
diff -r 10b2f60b70f0 -r 0284a7d083be src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- 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
diff -r 10b2f60b70f0 -r 0284a7d083be src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- 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" ^
diff -r 10b2f60b70f0 -r 0284a7d083be src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- 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"