1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
     1.3 @@ -2663,24 +2663,30 @@
     1.4      (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
     1.5      val _ = print_modes options thy' modes
     1.6      val _ = print_step options "Defining executable functions..."
     1.7 -    val thy'' = fold (#define_functions (dest_steps steps) options preds) modes thy'
     1.8 -      |> Theory.checkpoint
     1.9 +    val thy'' =
    1.10 +      Output.cond_timeit true "Defining executable functions..."
    1.11 +      (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
    1.12 +      |> Theory.checkpoint)
    1.13      val _ = print_step options "Compiling equations..."
    1.14      val compiled_terms =
    1.15 -      compile_preds (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses
    1.16 +      Output.cond_timeit true "Compiling equations...." (fn _ =>
    1.17 +      compile_preds (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses)
    1.18      val _ = print_compiled_terms options thy'' compiled_terms
    1.19      val _ = print_step options "Proving equations..."
    1.20      val result_thms =
    1.21 -      #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms
    1.22 +      Output.cond_timeit true "Proving equations...." (fn _ =>
    1.23 +      #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
    1.24      val result_thms' = #add_code_equations (dest_steps steps) thy'' preds
    1.25        (maps_modes result_thms)
    1.26      val qname = #qname (dest_steps steps)
    1.27      val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
    1.28        (fn thm => Context.mapping (Code.add_eqn thm) I))))
    1.29 -    val thy''' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
    1.30 +    val thy''' =
    1.31 +      Output.cond_timeit true "Setting code equations...." (fn _ =>
    1.32 +      fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
    1.33        [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
    1.34          [attrib thy ])] thy))
    1.35 -      result_thms' thy'' |> Theory.checkpoint
    1.36 +      result_thms' thy'' |> Theory.checkpoint)
    1.37    in
    1.38      thy'''
    1.39    end