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