# 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