src/Pure/sorts.ML

 Type classes and sorts.
 *)
 
 signature SORTS =
 sig
-  val str_of_sort: sort -> string
-  val str_of_arity: string * sort list * sort -> string
   val eq_sort: sort * sort -> bool
   val mem_sort: sort * sort list -> bool
   val subset_sort: sort list * sort list -> bool
   val eq_set_sort: sort list * sort list -> bool
   val ins_sort: sort * sort list -> sort list

   val inter_sort: classes -> sort * sort -> sort
   val norm_sort: classes -> sort -> sort
   val of_sort: classes * arities -> typ * sort -> bool
   exception DOMAIN of string * class
   val mg_domain: classes * arities -> string -> sort -> sort list  (*exception DOMAIN*)
-  val witness_sorts: classes * arities -> string list
-    -> sort list -> sort list -> (typ * sort) list
+  val witness_sorts: classes * arities -> string list ->
+    sort list -> sort list -> (typ * sort) list
 end;
 
 structure Sorts: SORTS =
 struct
 

   represented by lists of classes.  Normal forms of sorts are sorted
   lists of minimal classes (wrt. current class inclusion).
 
   (types already defined in Pure/term.ML)
 *)
-
-
-(* simple printing -- lacks pretty printing, translations etc. *)
-
-fun str_of_sort [c] = c
-  | str_of_sort cs = Library.enclose "{" "}" (Library.commas cs);
-
-fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
-  | str_of_arity (t, Ss, S) = t ^ " :: " ^
-      Library.enclose "(" ")" (Library.commas (map str_of_sort Ss)) ^ " " ^ str_of_sort S;
 
 
 (* equality, membership and insertion of sorts *)
 
 fun eq_sort ([]: sort, []) = true

 
 
 
 (** witness_sorts **)
 
-fun witness_sorts_aux (classes, arities) log_types hyps sorts =
+local
+
+fun witness_aux (classes, arities) log_types hyps sorts =
   let
     val top_witn = (propT, []);
     fun le S1 S2 = sort_le classes (S1, S2);
     fun get_solved S2 (T, S1) = if le S1 S2 then Some (T, S2) else None;
     fun get_hyp S2 S1 = if le S1 S2 then Some (TFree ("'hyp", S1), S2) else None;

                 end
           | None => witn_types path ts (solved_failed, S));
 
   in witn_sorts [] (([], []), sorts) end;
 
+fun str_of_sort [c] = c
+  | str_of_sort cs = enclose "{" "}" (commas cs);
+
+in
 
 fun witness_sorts (classes, arities) log_types hyps sorts =
   let
     (*double check result of witness search*)
     fun check_result None = None
       | check_result (Some (T, S)) =
           if of_sort (classes, arities) (T, S) then Some (T, S)
           else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
-  in mapfilter check_result (#2 (witness_sorts_aux (classes, arities) log_types hyps sorts)) end;
-
+  in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
 
 end;
+
+end;