src/HOL/Tools/function_package/fundef_prep.ML

       val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
 
       val ((R, RIntro_thmss, R_elim), lthy) = 
           PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
-      val lthy = PROFILE "abbrev"
+      val (_, lthy) = PROFILE "abbrev"
         (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
 
       val newthy = ProofContext.theory_of lthy
       val clauses = map (transfer_clause_ctx newthy) clauses