| changeset 42288 | 2074b31650e6 |
| parent 42287 | d98eb048a2e4 |
| child 42290 | b1f544c84040 |
--- a/src/Pure/sign.ML Fri Apr 08 14:20:57 2011 +0200 +++ b/src/Pure/sign.ML Fri Apr 08 15:02:11 2011 +0200 @@ -468,7 +468,7 @@ local -fun mk trs = map Syntax.mk_trfun trs; +fun mk trs = map Syntax_Ext.mk_trfun trs; fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) = map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's));