src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17775 2679ba74411f
parent 17772 818cec5f82a4
child 17997 6c0fe78624d9
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Oct 07 15:08:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Oct 07 17:57:21 2005 +0200
     1.3 @@ -156,27 +156,9 @@
     1.4  	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
     1.5      end
     1.6  
     1.7 -
     1.8 -(*****************************************************)
     1.9 -(* get names of clasimp axioms used                  *)
    1.10 -(*****************************************************)
    1.11 -
    1.12 +(* get names of clasimp axioms used*)
    1.13   fun get_axiom_names step_nums clause_arr =
    1.14 -   let 
    1.15 -     (* not sure why this is necessary again, but seems to be *)
    1.16 -      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.17 -  
    1.18 -     (***********************************************)
    1.19 -     (* here need to add the clauses from clause_arr*)
    1.20 -     (***********************************************)
    1.21 -  
    1.22 -      val clasimp_names_cls = get_clasimp_cls clause_arr step_nums 
    1.23 -      val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
    1.24 -      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.25 -   in
    1.26 -      clasimp_names
    1.27 -   end
    1.28 -   
    1.29 +   map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums);   
    1.30  
    1.31  fun get_axiom_names_spass proofstr clause_arr =
    1.32    let (* parse spass proof into datatype *)
    1.33 @@ -227,9 +209,7 @@
    1.34  fun addvars c (a,b)  = (a,b,c)
    1.35  
    1.36  fun get_axioms_used proof_steps thms clause_arr  =
    1.37 -  let 
    1.38 -     val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.39 -     val axioms = (List.filter is_axiom) proof_steps
    1.40 + let val axioms = (List.filter is_axiom) proof_steps
    1.41       val step_nums = get_step_nums axioms []
    1.42  
    1.43       val clauses = make_clauses thms    (*FIXME: must this be repeated??*)
    1.44 @@ -266,9 +246,9 @@
    1.45       val extra_with_vars = if (not (extra_metas = []) ) 
    1.46  			   then ListPair.zip (extra_metas,extra_vars)
    1.47  			   else []
    1.48 -  in
    1.49 -     (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
    1.50 -  end;
    1.51 + in
    1.52 +    (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
    1.53 + end;
    1.54                                              
    1.55  
    1.56  (*********************************************************************)
    1.57 @@ -277,7 +257,7 @@
    1.58  (*********************************************************************)
    1.59  
    1.60  fun rules_to_string [] = "NONE"
    1.61 -  | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
    1.62 +  | rules_to_string xs = space_implode "  " xs
    1.63  
    1.64  
    1.65  (*The signal handler in watcher.ML must be able to read the output of this.*)