adapted to qualified names;

--- 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 

--- a/TFL/tfl.sml	Fri Oct 17 18:03:46 1997 +0200
+++ b/TFL/tfl.sml	Fri Oct 17 18:14:48 1997 +0200
@@ -219,7 +219,8 @@
           in (map v_to_pats pref_patl, tm)
           end
      else
-     let val pty as Type (ty_name,_) = type_of p
+     let val pty as Type (full_ty_name,_) = type_of p;
+         val ty_name = NameSpace.base full_ty_name;
      in
      case (ty_info ty_name)
      of None => mk_case_fail("Not a known datatype: "^ty_name)
@@ -299,7 +300,7 @@
              of [] => ()
           | L => mk_functional_err("The following rows (counting from zero)\
                                    \ are inaccessible: "^stringize L)
- in {functional = Abs(fname, ftype, 
+ in {functional = Abs(NameSpace.base fname, ftype,
 		      abstract_over (fcon, 
 				     absfree(aname,atype, case_tm))),
      pats = patts2}
@@ -551,7 +552,8 @@
           in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
           end
      else                     (* column 0 is all constructors *)
-     let val Type (ty_name,_) = type_of p
+     let val Type (full_ty_name,_) = type_of p;
+         val ty_name = NameSpace.base full_ty_name;
      in
      case (ty_info ty_name)
      of None => fail("Not a known datatype: "^ty_name)