author | wenzelm |
Wed, 02 Aug 2006 22:26:56 +0200 | |
changeset 20302 | 265b2342cf21 |
parent 20301 | 66b2a1f16bbb |
child 20303 | e25d5a2a50bc |
--- 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