changeset 3610 | 7e5300420b03 |
parent 2867 | 0aa5a3cd4550 |
child 3835 | 9a5a4e123859 |
--- a/src/FOL/cladata.ML Wed Aug 06 00:39:13 1997 +0200 +++ b/src/FOL/cladata.ML Wed Aug 06 00:41:40 1997 +0200 @@ -61,6 +61,11 @@ claset := FOL_cs; +fun claset_of tname = + case get_thydata tname "claset" of + None => empty_cs + | Some (CS_DATA cs) => cs; + (*** Applying BlastFun to create Blast_tac ***) structure Blast_Data = struct