| changeset 20302 | 265b2342cf21 |
| parent 20232 | 31998a8c7f25 |
| child 21687 | f689f729afab |
--- a/src/Pure/tactic.ML Wed Aug 02 22:26:55 2006 +0200 +++ b/src/Pure/tactic.ML Wed Aug 02 22:26:56 2006 +0200 @@ -265,7 +265,7 @@ end; fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule' - (st, i, map (apfst Syntax.indexname) sinsts, rule); + (st, i, map (apfst Syntax.read_indexname) sinsts, rule); (* Like lift_inst_rule but takes terms, not strings, where the terms may contain