TFL/post.sml
changeset 3927 27c63b757af5
parent 3572 5ec1589eac1b
child 3978 7e1cfed19d94
--- a/TFL/post.sml	Fri Oct 17 18:03:46 1997 +0200
+++ b/TFL/post.sml	Fri Oct 17 18:14:48 1997 +0200
@@ -17,10 +17,10 @@
                            -> {induction:thm, rules:thm, TCs:term list list} 
                            -> {induction:thm, rules:thm, nested_tcs:thm list}
 
-   val define_i : theory -> string -> term -> term list
+   val define_i : theory -> xstring -> term -> term list
                   -> theory * Prim.pattern list
 
-   val define   : theory -> string -> string -> string list 
+   val define   : theory -> xstring -> string -> string list 
                   -> theory * Prim.pattern list
 
    val simplify_defn : simpset * thm list