| changeset 24244 | d7ee11ba1534 |
| parent 23539 | df5440e241a1 |
| child 25939 | ddea202704b4 |
--- a/src/Pure/tactic.ML Mon Aug 13 18:10:20 2007 +0200 +++ b/src/Pure/tactic.ML Mon Aug 13 18:10:22 2007 +0200 @@ -245,7 +245,7 @@ end; fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule' - (st, i, map (apfst Syntax.read_indexname) sinsts, rule); + (st, i, map (apfst Lexicon.read_indexname) sinsts, rule); (* Like lift_inst_rule but takes terms, not strings, where the terms may contain