changeset 58634 | 9f10d82e8188 |
parent 55990 | 41c6b99c5fb7 |
child 58816 | aab139c0003f |
--- a/src/HOL/Tools/Function/function_core.ML Wed Oct 08 14:34:30 2014 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Wed Oct 08 17:09:07 2014 +0200 @@ -873,7 +873,7 @@ val cert = cterm_of (Proof_Context.theory_of lthy) val xclauses = PROFILE "xclauses" - (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees + (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss val complete =