src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15739 bb2acfed8212
parent 15700 970e0293dfb3
child 15774 9df37a0e935d
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 15 17:03:35 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 15 18:16:05 2005 +0200
     1.3 @@ -108,9 +108,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -
     1.8 -
     1.9 -
    1.10  fun is_axiom ( num:int,Axiom, str) = true
    1.11  |   is_axiom (num, _,_) = false
    1.12  
    1.13 @@ -128,8 +125,7 @@
    1.14  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
    1.15  *)
    1.16  (*FIX - should this have vars in it? *)
    1.17 -fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) 
    1.18 -                                   
    1.19 +fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))                        
    1.20                                 in 
    1.21                                     true
    1.22                                end
    1.23 @@ -155,9 +151,6 @@
    1.24  fun thmstrings [] str = str
    1.25  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    1.26  
    1.27 -fun onelist [] newlist = newlist
    1.28 -|   onelist (x::xs) newlist = onelist xs (newlist@x)
    1.29 -
    1.30  
    1.31   fun get_axioms_used proof_steps thmstring = let 
    1.32                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.33 @@ -175,7 +168,7 @@
    1.34                                             
    1.35                                              val distvars = distinct (fold append vars [])
    1.36                                              val clause_terms = map prop_of clauses  
    1.37 -                                            val clause_frees = onelist (map term_frees clause_terms) []
    1.38 +                                            val clause_frees = List.concat (map term_frees clause_terms)
    1.39  
    1.40                                              val frees = map lit_string_with_nums clause_frees;
    1.41  
    1.42 @@ -313,7 +306,7 @@
    1.43                                                    val _ = TextIO.output (outfile, (thmstring))
    1.44                                                    val _ =  TextIO.closeOut outfile
    1.45                                                    val proofextract = extract_proof proofstr
    1.46 -                                                  val tokens = fst(lex proofextract)
    1.47 +                                                  val tokens = #1(lex proofextract)
    1.48                                                       
    1.49                                                (***********************************)
    1.50                                                (* parse spass proof into datatype *)
    1.51 @@ -352,8 +345,8 @@
    1.52                                                    (* turn the proof into a string *)
    1.53                                                    val reconProofStr = proofs_to_string proof ""
    1.54                                                    (* do the bit for the Isabelle ordered axioms at the top *)
    1.55 -                                                  val ax_nums = map fst numcls
    1.56 -                                                  val ax_strs = map get_meta_lits_bracket (map snd numcls)
    1.57 +                                                  val ax_nums = map #1 numcls
    1.58 +                                                  val ax_strs = map get_meta_lits_bracket (map #2 numcls)
    1.59                                                    val numcls_strs = zip ax_nums ax_strs
    1.60                                                    val num_cls_vars =  map (addvars vars) numcls_strs;
    1.61                                                    val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
    1.62 @@ -449,7 +442,7 @@
    1.63  
    1.64  
    1.65   val number_list_step =
    1.66 -        ( number ++ many ((a (Other ",") ++ number)>> snd))
    1.67 +        ( number ++ many ((a (Other ",") ++ number)>> #2))
    1.68          >> (fn (a,b) => (a::b))
    1.69          
    1.70   val numberlist_step = a (Other "[")  ++ a (Other "]")
    1.71 @@ -510,9 +503,9 @@
    1.72      
    1.73   val lines_step = many linestep
    1.74  
    1.75 - val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst
    1.76 + val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
    1.77      
    1.78 - val parse_step = fst o alllines_step
    1.79 + val parse_step = #1 o alllines_step
    1.80  
    1.81  
    1.82   (*
    1.83 @@ -702,7 +695,7 @@
    1.84  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)))";
    1.85  *)
    1.86  
    1.87 -fun apply_res_thm str goalstring  = let val tokens = fst (lex str);
    1.88 +fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
    1.89  
    1.90                                     val (frees,recon_steps) = parse_step tokens 
    1.91                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)