diff -r 91a91790899a -r 2cccd0e3e9ea TFL/thry.sig
--- a/TFL/thry.sig	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/thry.sig	Thu Jun 05 13:27:28 1997 +0200
@@ -6,7 +6,6 @@
 
 signature Thry_sig =
 sig
-  structure USyntax : USyntax_sig
   val match_term : theory -> term -> term 
                     -> (term*term)list * (typ*typ)list
 
@@ -14,8 +13,6 @@
 
   val typecheck : theory -> term -> cterm
 
-  val make_definition: theory -> string -> term -> thm * theory
-
   (* Datatype facts of various flavours *)
   val match_info: theory -> string -> {constructors:term list,
                                      case_const:term} option