| changeset 63068 | 8b9401bfd9fd |
| parent 62680 | 646b84666a56 |
| child 63352 | 4eaf35781b23 |
--- a/src/Pure/Isar/interpretation.ML Thu Apr 28 11:47:01 2016 +0200 +++ b/src/Pure/Isar/interpretation.ML Thu Apr 28 15:42:52 2016 +0200 @@ -116,8 +116,7 @@ local -fun meta_rewrite eqns ctxt = - (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt); +fun meta_rewrite eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = let