| changeset 31365 | 7f65653e3d48 |
| parent 31358 | 3e640334a1b3 |
| parent 31323 | 89f218fcab2a |
| child 31794 | 71af1fd6a5e4 |
--- a/src/Pure/Isar/attrib.ML Tue Jun 02 14:00:24 2009 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Jun 02 14:38:10 2009 +0200 @@ -240,8 +240,7 @@ (* rename_abs *) -val rename_abs : (Context.generic * thm -> Context.generic * thm) parser = - Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'); +fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x; (* unfold / fold definitions *)