# HG changeset patch
# User blanchet
# Date 1281344634 -7200
# Node ID 577f138af235bb418027699cf85b61c6a07bf2df
# Parent  7497c22bb185e0dff57a7f8d705738d4138858ec
replace recursion with "fold"

diff -r 7497c22bb185 -r 577f138af235 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 10:39:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 11:03:54 2010 +0200
@@ -55,7 +55,7 @@
         let
           val args = OldTerm.term_frees body
           val Ts = map type_of args
-          val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+          val cT = Ts ---> T
           (* Forms a lambda-abstraction over the formal parameters *)
           val rhs =
             list_abs_free (map dest_Free args,
@@ -78,7 +78,7 @@
 
 (*Returns the vars of a theorem*)
 fun vars_of_thm th =
-  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
+  map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
 
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
@@ -181,7 +181,7 @@
             TrueI)
 
 (*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
+val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
 
 (*Given an abstraction over n variables, replace the bound variables by free
   ones. Return the body, along with the list of free variables.*)
@@ -197,7 +197,7 @@
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
 fun skolem_theorem_of_def thy rhs0 =
   let
-    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
+    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
     val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
@@ -205,7 +205,7 @@
       case hilbert of
         Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
       | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
-    val cex = Thm.cterm_of thy (HOLogic.exists_const T)
+    val cex = cterm_of thy (HOLogic.exists_const T)
     val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
     val conc =
       Drule.list_comb (rhs, frees)
diff -r 7497c22bb185 -r 577f138af235 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 09 10:39:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 09 11:03:54 2010 +0200
@@ -574,23 +574,21 @@
 
 fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
 
-(* FIXME: use "fold" instead *)
-fun translate _ _ _ thpairs [] = thpairs
-  | translate ctxt mode skolems thpairs ((fol_th, inf) :: infpairs) =
-      let val _ = trace_msg (fn () => "=============================================")
-          val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
-          val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
-          val th = Meson.flexflex_first_order (step ctxt mode skolems
-                                                    thpairs (fol_th, inf))
-          val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
-          val _ = trace_msg (fn () => "=============================================")
-          val n_metis_lits =
-            length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
-      in
-          if nprems_of th = n_metis_lits then ()
-          else raise METIS ("translate", "Proof reconstruction has gone wrong.");
-          translate ctxt mode skolems ((fol_th, th) :: thpairs) infpairs
-      end;
+fun translate_one ctxt mode skolems (fol_th, inf) thpairs =
+  let
+    val _ = trace_msg (fn () => "=============================================")
+    val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
+    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
+    val th = Meson.flexflex_first_order (step ctxt mode skolems
+                                              thpairs (fol_th, inf))
+    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+    val _ = trace_msg (fn () => "=============================================")
+    val n_metis_lits =
+      length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
+    val _ =
+      if nprems_of th = n_metis_lits then ()
+      else raise METIS ("translate", "Proof reconstruction has gone wrong.")
+  in (fol_th, th) :: thpairs end
 
 (*Determining which axiom clauses are actually used*)
 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
@@ -744,7 +742,7 @@
                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
                              (*add constraints arising from converting goal to clause form*)
                 val proof = Metis.Proof.proof mth
-                val result = translate ctxt' mode skolems axioms proof
+                val result = fold (translate_one ctxt' mode skolems) proof axioms
                 and used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used