changeset 24751 | dbb34a03af5a |
parent 24693 | fe88913f3706 |
child 24787 | df56433cc059 |
--- a/src/Pure/Isar/locale.ML Sat Sep 29 08:58:55 2007 +0200 +++ b/src/Pure/Isar/locale.ML Sat Sep 29 08:58:56 2007 +0200 @@ -45,6 +45,7 @@ val map_elem: ('a -> 'b) -> 'a element -> 'b element val intern: theory -> xstring -> string + val intern_expr: theory -> expr -> expr val extern: theory -> string -> xstring val init: string -> theory -> Proof.context