src/HOL/Tools/res_atp.ML
changeset 21888 c75a44597fb7
parent 21858 05f57309170c
child 21900 f386d7eb17d1
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Dec 19 19:34:35 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Dec 20 17:03:46 2006 +0100
     1.3 @@ -819,9 +819,9 @@
     1.4      Output.debug "Sent commands to watcher!"
     1.5    end
     1.6  
     1.7 -fun trace_array fname =
     1.8 +fun trace_vector fname =
     1.9    let val path = File.explode_platform_path fname
    1.10 -  in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
    1.11 +  in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
    1.12  
    1.13  (*Converting a subgoal into negated conjecture clauses*)
    1.14  fun neg_clauses th n =
    1.15 @@ -873,9 +873,9 @@
    1.16                  val arity_clauses = ResClause.arity_clause_thy thy tycons supers
    1.17                  val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.18                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.19 -                val thm_names = Array.fromList clnames
    1.20 +                val thm_names = Vector.fromList clnames
    1.21                  val _ = if !Output.show_debug_msgs
    1.22 -                        then trace_array (fname ^ "_thm_names") thm_names else ()
    1.23 +                        then trace_vector (fname ^ "_thm_names") thm_names else ()
    1.24              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
    1.25        val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
    1.26    in