TFL/post.sml

 
    val std_postprocessor : simpset -> theory 
                            -> {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 
                         -> theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}