# HG changeset patch
# User mengj
# Date 1129723173 -7200
# Node ID ac97527724ba91fa37f8140444fbba12f3b9c156
# Parent  c20e4bddcb11a34bfcda5c025d14eebfc2daf6cc
More functions are added to the signature of ResClause

diff -r c20e4bddcb11 -r ac97527724ba src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Oct 19 10:25:46 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Oct 19 13:59:33 2005 +0200
@@ -48,6 +48,19 @@
   val const_prefix : string
   val tconst_prefix : string 
   val class_prefix : string 
+
+  val union_all : ''a list list -> ''a list
+  val ascii_of : String.string -> String.string
+  val paren_pack : string list -> string
+  val bracket_pack : string list -> string
+  val make_schematic_var : String.string * int -> string
+  val make_fixed_var : String.string -> string
+  val make_schematic_type_var : string * int -> string
+  val make_fixed_type_var : string -> string
+  val make_fixed_const : String.string -> string		
+  val make_fixed_type_const : String.string -> string   
+  val make_type_class : String.string -> string
+
   end;
 
 structure ResClause: RES_CLAUSE =