author | haftmann |
Sat, 29 Sep 2007 08:58:56 +0200 | |
changeset 24751 | dbb34a03af5a |
parent 24750 | 95a315591af8 |
child 24752 | 8aec6154bb17 |
--- 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