--- a/src/HOL/Tools/ATP/AtpCommunication.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Tue Sep 20 18:43:39 2005 +0200
@@ -191,7 +191,7 @@
fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr =
SELECT_GOAL
- (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
+ (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num;
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue Sep 20 18:43:39 2005 +0200
@@ -130,8 +130,7 @@
(Pretty.setmp_margin 999 string_of_thm));
fun fake_thm_name th =
- Context.theory_name (theory_of_thm th) ^ "." ^
- ResLib.trim_ends (plain_string_of_thm th);
+ Context.theory_name (theory_of_thm th) ^ "." ^ unenclose (plain_string_of_thm th);
fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th)
else ("HOL.TrueI",TrueI)
--- a/src/HOL/Tools/ATP/watcher.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Sep 20 18:43:39 2005 +0200
@@ -270,7 +270,9 @@
fun prems_string_of th =
Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
-fun killChildren procs = List.app (ignore o Unix.reap) procs;
+fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
+
+fun killChildren procs = List.app (ignore o killChild) procs;
fun setupWatcher (thm,clause_arr) =
let
--- a/src/HOL/Tools/res_atp.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Sep 20 18:43:39 2005 +0200
@@ -61,30 +61,29 @@
(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
-fun tptp_inputs_tfrees thms n axclauses =
+fun tptp_inputs_tfrees thms n (axclauses,classrel_clauses,arity_clauses) =
let
- val _ = debug ("in tptp_inputs_tfrees 0")
val clss = map (ResClause.make_conjecture_clause_thm) thms
- val _ = debug ("in tptp_inputs_tfrees 1")
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
- val _ = debug ("in tptp_inputs_tfrees 2")
val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
- val _ = debug ("in tptp_inputs_tfrees 3")
- val probfile = prob_pathname() ^ "_" ^ string_of_int n
+ val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
+ val arity_cls = map ResClause.tptp_arity_clause arity_clauses
+ val probfile = prob_pathname() ^ "_" ^ Int.toString n
val out = TextIO.openOut(probfile)
in
ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
- ResLib.writeln_strs out (tfree_clss @ tptp_clss);
+ ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
TextIO.closeOut out;
debug probfile
end;
(* write out a subgoal in DFG format to the file "xxxx_N"*)
-fun dfg_inputs_tfrees thms n axclauses =
+fun dfg_inputs_tfrees thms n (axclauses,classrel_clauses,arity_clauses) =
let val clss = map (ResClause.make_conjecture_clause_thm) thms
- val probfile = prob_pathname() ^ "_" ^ (string_of_int n)
+ val probfile = prob_pathname() ^ "_" ^ (Int.toString n)
+ (*FIXME: classrel_clauses and arity_clauses*)
val _ = debug ("about to write out dfg prob file " ^ probfile)
- val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ string_of_int n)
+ val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
axclauses [] [] []
val out = TextIO.openOut(probfile)
in
@@ -104,7 +103,7 @@
val goalstring = proofstring (Sign.string_of_term sign sg_term)
val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
- val probfile = prob_pathname() ^ "_" ^ string_of_int n
+ val probfile = prob_pathname() ^ "_" ^ Int.toString n
val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
in
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ
@@ -151,34 +150,31 @@
debug "Sent commands to watcher!"
end
-(*We write out problem files for each subgoal, but work is repeated (skolemize)*)
-fun write_problem_files axclauses thm n =
+(*We write out problem files for each subgoal*)
+fun write_problem_files clause thm n =
if n=0 then ()
else
(SELECT_GOAL
- (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
+ (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
(if !prover = "spass"
- then dfg_inputs_tfrees (make_clauses negs) n axclauses
- else tptp_inputs_tfrees (make_clauses negs) n axclauses;
- write_problem_files axclauses thm (n-1);
+ then dfg_inputs_tfrees (make_clauses negs) n clause
+ else tptp_inputs_tfrees (make_clauses negs) n clause;
+ write_problem_files clause thm (n-1);
all_tac))]) n thm;
());
val last_watcher_pid = ref (NONE : Posix.Process.pid option);
-(******************************************************************)
-(* called in Isar automatically *)
-(* writes out the current clasimpset to a tptp file *)
-(* turns off xsymbol at start of function, restoring it at end *)
-(******************************************************************)
-(*FIX changed to clasimp_file *)
+
+(*writes out the current clasimpset to a tptp file;
+ turns off xsymbol at start of function, restoring it at end *)
val isar_atp = setmp print_mode []
(fn (ctxt, thm) =>
if Thm.no_prems thm then ()
else
let
- val _= debug ("in isar_atp")
+ val _= debug "in isar_atp"
val thy = ProofContext.theory_of ctxt
val prems = Thm.prems_of thm
val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
@@ -193,13 +189,17 @@
val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems)
(*FIXME: hack!! need to consider relevance for all prems*)
val _ = debug ("claset and simprules total clauses = " ^
- string_of_int (Array.length clause_arr))
+ Int.toString (Array.length clause_arr))
+ val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy
+ val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
+ val arity_clauses = ResTypesSorts.arity_clause_thy thy
+ val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
in
last_watcher_pid := SOME pid;
debug ("subgoals: " ^ prems_string);
debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
- write_problem_files axclauses thm (length prems);
+ write_problem_files (axclauses,classrel_clauses,arity_clauses) thm (length prems);
watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
end);
@@ -207,10 +207,14 @@
(fn (ctxt, thm) =>
if Thm.no_prems thm then ()
else
- let val prems = Thm.prems_of thm
- val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems)
+ let
+ val prems = Thm.prems_of thm
+ val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems)
+ val thy = ProofContext.theory_of ctxt
+ val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy
+ val arity_clauses = ResTypesSorts.arity_clause_thy thy
in
- write_problem_files axclauses thm (length prems)
+ write_problem_files (axclauses,classrel_clauses,arity_clauses) thm (length prems)
end);
@@ -228,10 +232,10 @@
debug ("subgoals in isar_atp: " ^
Pretty.string_of (ProofContext.pretty_term ctxt
(Logic.mk_conjunction_list (Thm.prems_of goal))));
- debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
+ debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
debug ("current theory: " ^ Context.theory_name thy);
hook_count := !hook_count +1;
- debug ("in hook for time: " ^(string_of_int (!hook_count)) );
+ debug ("in hook for time: " ^(Int.toString (!hook_count)) );
ResClause.init thy;
if !destdir = "" then isar_atp (ctxt, goal)
else isar_atp_writeonly (ctxt, goal)
--- a/src/HOL/Tools/res_clause.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Tue Sep 20 18:43:39 2005 +0200
@@ -70,8 +70,8 @@
val tfree_prefix = "t_";
val clause_prefix = "cls_";
-val arclause_prefix = "arcls_"
-val clrelclause_prefix = "relcls_";
+val arclause_prefix = "clsarity_"
+val clrelclause_prefix = "clsrel_";
val const_prefix = "c_";
val tconst_prefix = "tc_";
@@ -124,13 +124,19 @@
end;
+(* convert a list of strings into one single string; surrounded by brackets *)
+fun paren_pack strings = "(" ^ commas strings ^ ")";
+
+fun bracket_pack strings = "[" ^ commas strings ^ "]";
+
+
(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
else error ("trim_type: Malformed type variable encountered: " ^ s);
fun ascii_of_indexname (v,0) = ascii_of v
- | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i;
+ | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
@@ -287,7 +293,7 @@
val funcs' = ResLib.flat_noDup funcslist
val t = make_fixed_type_const a
in
- ((t ^ (ResLib.list_to_string folTyps)),(ts', (t, length Ts)::funcs') )
+ ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
end
| type_of (TFree (a, s)) =
let val t = make_fixed_type_var a
@@ -587,7 +593,7 @@
fun get_TVars 0 = []
- | get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n-1);
+ | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1);
@@ -677,8 +683,8 @@
let val terms' = map string_of_term terms
in
if !keep_types andalso typ<>""
- then name ^ (ResLib.list_to_string (terms' @ [typ]))
- else name ^ (ResLib.list_to_string terms')
+ then name ^ (paren_pack (terms' @ [typ]))
+ else name ^ (paren_pack terms')
end;
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
@@ -689,16 +695,16 @@
let val terms_as_strings = map string_of_term terms
in
if !keep_types andalso typ<>""
- then name ^ (ResLib.list_to_string (terms_as_strings @ [typ]))
- else name ^ (ResLib.list_to_string terms_as_strings)
+ then name ^ (paren_pack (terms_as_strings @ [typ]))
+ else name ^ (paren_pack terms_as_strings)
end;
fun string_of_clausename (cls_id,ax_name) =
- clause_prefix ^ ascii_of ax_name ^ "_" ^ string_of_int cls_id;
+ clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
fun string_of_type_clsname (cls_id,ax_name,idx) =
- string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (string_of_int idx);
+ string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
(********************************)
@@ -796,8 +802,8 @@
let val terms_as_strings = map string_of_term terms
in
if !keep_types andalso typ<>""
- then name ^ (ResLib.list_to_string (terms_as_strings @ [typ]))
- else name ^ (ResLib.list_to_string terms_as_strings)
+ then name ^ (paren_pack (terms_as_strings @ [typ]))
+ else name ^ (paren_pack terms_as_strings)
end;
@@ -826,7 +832,7 @@
cls_str :: (typ_clss 0 tfree_lits)
end;
-fun string_of_arity (name, num) = name ^ "," ^ (string_of_int num)
+fun string_of_arity (name, num) = name ^ "," ^ (Int.toString num)
fun string_of_preds preds =
"predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
@@ -924,42 +930,43 @@
fun string_of_arClauseID (ArityClause arcls) =
- arclause_prefix ^ string_of_int(#clause_id arcls);
-
-fun string_of_arLit (TConsLit(b,(c,t,args))) =
- let val pol = if b then "++" else "--"
- val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
- in
- pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
- end
- | string_of_arLit (TVarLit(b,(c,str))) =
- let val pol = if b then "++" else "--"
- in
- pol ^ c ^ "(" ^ str ^ ")"
- end;
-
-
-fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
-
-
-fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
-
+ arclause_prefix ^ Int.toString(#clause_id arcls);
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
-(*FIX: would this have variables in a forall? *)
+(*FIXME!!! currently is TPTP format!*)
+fun dfg_of_arLit (TConsLit(b,(c,t,args))) =
+ let val pol = if b then "++" else "--"
+ val arg_strs = (case args of [] => "" | _ => paren_pack args)
+ in
+ pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
+ end
+ | dfg_of_arLit (TVarLit(b,(c,str))) =
+ let val pol = if b then "++" else "--"
+ in
+ pol ^ c ^ "(" ^ str ^ ")"
+ end;
+
+
+fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls);
+
+
+fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls);
+
+
+
+(*FIXME: would this have variables in a forall? *)
fun dfg_arity_clause arcls =
- let val arcls_id = string_of_arClauseID arcls
- val concl_lit = string_of_conclLit arcls
- val prems_lits = strings_of_premLits arcls
- val knd = string_of_arKind arcls
- val all_lits = concl_lit :: prems_lits
- in
-
- "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^
- arcls_id ^ ")."
- end;
+ let val arcls_id = string_of_arClauseID arcls
+ val concl_lit = dfg_of_conclLit arcls
+ val prems_lits = dfg_of_premLits arcls
+ val knd = string_of_arKind arcls
+ val all_lits = concl_lit :: prems_lits
+ in
+ "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (bracket_pack all_lits) ^ ")),\n" ^
+ arcls_id ^ ")."
+ end;
(********************************)
@@ -1009,7 +1016,7 @@
val cls_id = get_clause_id cls
val ax_name = get_axiomName cls
val knd = string_of_kind cls
- val lits_str = ResLib.list_to_string' lits
+ val lits_str = bracket_pack lits
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str)
fun typ_clss k [] = []
| typ_clss k (tfree :: tfrees) =
@@ -1025,7 +1032,7 @@
val cls_id = get_clause_id cls
val ax_name = get_axiomName cls
val knd = string_of_kind cls
- val lits_str = ResLib.list_to_string' lits
+ val lits_str = bracket_pack lits
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str)
in
(cls_str,tfree_lits)
@@ -1039,40 +1046,32 @@
val tptp_clauses2str = ResLib.list2str_sep delim;
-fun string_of_arClauseID (ArityClause arcls) =
- arclause_prefix ^ string_of_int(#clause_id arcls);
-
-
-fun string_of_arLit (TConsLit(b,(c,t,args))) =
- let val pol = if b then "++" else "--"
- val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
- in
- pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
- end
- | string_of_arLit (TVarLit(b,(c,str))) =
- let val pol = if b then "++" else "--"
- in
- pol ^ c ^ "(" ^ str ^ ")"
- end;
+fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
+ let val pol = if b then "++" else "--"
+ val arg_strs = (case args of [] => "" | _ => paren_pack args)
+ in
+ pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
+ end
+ | tptp_of_arLit (TVarLit(b,(c,str))) =
+ let val pol = if b then "++" else "--"
+ in
+ pol ^ c ^ "(" ^ str ^ ")"
+ end;
-fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
+fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls);
-fun strings_of_premLits (ArityClause arcls) =
- map string_of_arLit (#premLits arcls);
+fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls);
-
-fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
-
fun tptp_arity_clause arcls =
let val arcls_id = string_of_arClauseID arcls
- val concl_lit = string_of_conclLit arcls
- val prems_lits = strings_of_premLits arcls
+ val concl_lit = tptp_of_conclLit arcls
+ val prems_lits = tptp_of_premLits arcls
val knd = string_of_arKind arcls
val all_lits = concl_lit :: prems_lits
in
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^
- (ResLib.list_to_string' all_lits) ^ ")."
+ (bracket_pack all_lits) ^ ")."
end;
fun tptp_classrelLits sub sup =
@@ -1084,7 +1083,7 @@
fun tptp_classrelClause (ClassrelClause cls) =
- let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls)
+ let val relcls_id = clrelclause_prefix ^ Int.toString(#clause_id cls)
val sub = #subclass cls
val sup = #superclass cls
val lits = tptp_classrelLits sub sup
--- a/src/HOL/Tools/res_lib.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML Tue Sep 20 18:43:39 2005 +0200
@@ -8,16 +8,12 @@
signature RES_LIB =
sig
-val atomize_tac : int -> tactic
val flat_noDup : ''a list list -> ''a list
val helper_path : string -> string -> string
val list2str_sep : string -> string list -> string
-val list_to_string : string list -> string
-val list_to_string' : string list -> string
val no_rep_add : ''a -> ''a list -> ''a list
val no_rep_app : ''a list -> ''a list -> ''a list
val pair_ins : 'a -> 'b list -> ('a * 'b) list
-val trim_ends : string -> string
val write_strs : TextIO.outstream -> TextIO.vector list -> unit
val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
val intOfPid : Posix.Process.pid -> Int.int
@@ -28,42 +24,6 @@
structure ResLib : RES_LIB =
struct
-val atomize_tac =
- SUBGOAL
- (fn (prop,_) =>
- let val ts = Logic.strip_assums_hyp prop
- val atom = ObjectLogic.atomize_thm o forall_intr_vars
- in EVERY1
- [METAHYPS
- (fn hyps => cut_facts_tac (map atom hyps) 1),
- REPEAT_DETERM_N (length ts) o (etac thin_rl)]
- end);
-
-(*Remove both ends from the string (presumably quotation marks?)*)
-fun trim_ends s = String.substring(s,1,String.size s - 2);
-
-
-(* convert a list of strings into one single string; surrounded by brackets *)
-fun list_to_string strings =
-let
- fun str_of [s] = s
- | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
- | str_of _ = ""
-in
- "(" ^ str_of strings ^ ")"
-end;
-
-fun list_to_string' strings =
-let
- fun str_of [s] = s
- | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
- | str_of _ = ""
-in
- "[" ^ str_of strings ^ "]"
-end;
-
-(* remove some chars (not allowed by TPTP format) from a string *)
-
fun no_rep_add x [] = [x]
| no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
--- a/src/HOL/Tools/res_types_sorts.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/res_types_sorts.ML Tue Sep 20 18:43:39 2005 +0200
@@ -10,16 +10,11 @@
sig
exception ARITIES of string
val arity_clause: string * (string * string list list) list -> ResClause.arityClause list
- val arity_clause_thy: theory -> ResClause.arityClause list list * (string * 'a list) list
+ val arity_clause_thy: theory -> ResClause.arityClause list
type classrelClauses
val classrel_clause: string * string list -> ResClause.classrelClause list
val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list
- val classrel_clauses_thy: theory -> ResClause.classrelClause list list
- val multi_arity_clause:
- (string * (string * string list list) list) list ->
- (string * 'a list) list ->
- ResClause.arityClause list list * (string * 'a list) list
- val tptp_arity_clause_thy: theory -> string list list
+ val classrel_clauses_thy: theory -> ResClause.classrelClause list
end;
structure ResTypesSorts: RES_TYPES_SORTS =
@@ -38,15 +33,12 @@
| multi_arity_clause ((tcon, []) :: tcons_ars) expts =
multi_arity_clause tcons_ars ((tcon, []) :: expts)
| multi_arity_clause (tcon_ar :: tcons_ars) expts =
- let val result = multi_arity_clause tcons_ars expts
- in ((arity_clause tcon_ar :: fst result), snd result) end;
+ let val (cls,ary) = multi_arity_clause tcons_ars expts
+ in ((arity_clause tcon_ar @ cls), ary) end;
fun arity_clause_thy thy =
let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
- in multi_arity_clause (Symtab.dest arities) [] end;
-
-fun tptp_arity_clause_thy thy =
- map (map ResClause.tptp_arity_clause) (#1 (arity_clause_thy thy));
+ in #1 (multi_arity_clause (Symtab.dest arities) []) end;
(* Isabelle classes *)
@@ -56,9 +48,6 @@
val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
val classrel_clause = ResClause.classrelClauses_of;
fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C);
-val classrel_clauses_thy = classrel_clauses_classrel o classrel_of;
-
-val tptp_classrel_clauses_thy =
- map (map ResClause.tptp_classrelClause) o classrel_clauses_thy;
+val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of;
end;