--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Fri Apr 15 17:03:35 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Fri Apr 15 18:16:05 2005 +0200
@@ -228,28 +228,27 @@
fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
-fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
+fun lit_string sg t =
+ let val termstr = Sign.string_of_term sg t
val exp_term = explode termstr
in
implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
end
-fun get_meta_lits thm = map lit_string (prems_of thm)
-
+fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
+fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
-fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
-
-fun lit_string_bracket t = let val termstr = (Sign.string_of_term Mainsign ) t
+fun lit_string_bracket sg t =
+ let val termstr = Sign.string_of_term sg t
val exp_term = explode termstr
in
implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term)
end
-fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
-
-
+fun get_meta_lits_bracket thm =
+ map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
fun apply_rule rule [] thm = thm
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Apr 15 17:03:35 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Apr 15 18:16:05 2005 +0200
@@ -108,9 +108,6 @@
-
-
-
fun is_axiom ( num:int,Axiom, str) = true
| is_axiom (num, _,_) = false
@@ -128,8 +125,7 @@
| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
*)
(*FIX - should this have vars in it? *)
-fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))
-
+fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))
in
true
end
@@ -155,9 +151,6 @@
fun thmstrings [] str = str
| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
-fun onelist [] newlist = newlist
-| onelist (x::xs) newlist = onelist xs (newlist@x)
-
fun get_axioms_used proof_steps thmstring = let
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
@@ -175,7 +168,7 @@
val distvars = distinct (fold append vars [])
val clause_terms = map prop_of clauses
- val clause_frees = onelist (map term_frees clause_terms) []
+ val clause_frees = List.concat (map term_frees clause_terms)
val frees = map lit_string_with_nums clause_frees;
@@ -313,7 +306,7 @@
val _ = TextIO.output (outfile, (thmstring))
val _ = TextIO.closeOut outfile
val proofextract = extract_proof proofstr
- val tokens = fst(lex proofextract)
+ val tokens = #1(lex proofextract)
(***********************************)
(* parse spass proof into datatype *)
@@ -352,8 +345,8 @@
(* turn the proof into a string *)
val reconProofStr = proofs_to_string proof ""
(* do the bit for the Isabelle ordered axioms at the top *)
- val ax_nums = map fst numcls
- val ax_strs = map get_meta_lits_bracket (map snd numcls)
+ val ax_nums = map #1 numcls
+ val ax_strs = map get_meta_lits_bracket (map #2 numcls)
val numcls_strs = zip ax_nums ax_strs
val num_cls_vars = map (addvars vars) numcls_strs;
val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
@@ -449,7 +442,7 @@
val number_list_step =
- ( number ++ many ((a (Other ",") ++ number)>> snd))
+ ( number ++ many ((a (Other ",") ++ number)>> #2))
>> (fn (a,b) => (a::b))
val numberlist_step = a (Other "[") ++ a (Other "]")
@@ -510,9 +503,9 @@
val lines_step = many linestep
- val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst
+ val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
- val parse_step = fst o alllines_step
+ val parse_step = #1 o alllines_step
(*
@@ -702,7 +695,7 @@
val thmstring = " (ALL xa::'a::type. (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
*)
-fun apply_res_thm str goalstring = let val tokens = fst (lex str);
+fun apply_res_thm str goalstring = let val tokens = #1 (lex str);
val (frees,recon_steps) = parse_step tokens
val isar_str = to_isar_proof (frees, recon_steps, goalstring)
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 17:03:35 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 18:16:05 2005 +0200
@@ -141,6 +141,7 @@
(* Reconstruct a factoring step *)
(*************************************)
+(*FIXME: share code with that in Tools/reconstruction.ML*)
fun follow_factor clause lit1 lit2 allvars thml clause_strs=
let
val th = Recon_Base.assoc clause thml
@@ -148,7 +149,7 @@
val sign = sign_of_thm th
val fac1 = get_nth (lit1+1) prems
val fac2 = get_nth (lit2+1) prems
- val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
+ val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
val newenv = getnewenv unif_env
val envlist = Envir.alist_of newenv