# 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"