# HG changeset patch
# User wenzelm
# Date 881507136 -3600
# Node ID 0a32020760fa2830257837849d0e3fe50dfa4d22
# Parent  7049ca8f912e1e885b5f2429335064845cf2fc60
added print_claset;

diff -r 7049ca8f912e -r 0a32020760fa src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Dec 06 17:06:21 1997 +0100
+++ b/src/Provers/classical.ML	Sun Dec 07 16:05:36 1997 +0100
@@ -47,6 +47,7 @@
   type claset
   val empty_cs: claset
   val print_cs: claset -> unit
+  val print_claset: theory -> unit
   val rep_claset:
     claset -> {safeIs: thm list, safeEs: thm list,
 		 hazIs: thm list, hazEs: thm list,
@@ -736,6 +737,8 @@
 
 (* access claset *)
 
+fun print_claset thy = Display.print_data thy clasetK;
+
 fun claset_ref_of_sg sg =
   (case Sign.get_data sg clasetK of
     ClasetData (ref (CSData r)) => r