--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 27 12:22:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 27 12:23:00 2010 +0200
@@ -315,8 +315,9 @@
val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
- val res = (map translate_intro intros', constant_table')
- in res end
+ in
+ (map translate_intro intros', constant_table')
+ end
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -669,7 +670,9 @@
|> (if #ensure_groundness options then
add_ground_predicates ctxt (#limited_types options)
else I)
+ |> tap (fn _ => tracing "Adding limited predicates...")
|> add_limited_predicates (#limited_predicates options)
+ |> tap (fn _ => tracing "Replacing predicates...")
|> apfst (fold replace (#replacing options))
|> apfst (reorder_manually (#manual_reorder options))
|> apfst rename_vars_program