src/Provers/classical.ML
changeset 4380 0a32020760fa
parent 4271 3a82492e70c5
child 4392 ea41d9c1b0ef
--- 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