# HG changeset patch
# User blanchet
# Date 1288083424 -7200
# Node ID 04a05b2a7a369b6bc86f140835b53d4f5547052a
# Parent  23adc2138704d6816a8f6a060535798889b6349c
no need to encode theorem number twice in skolem names

diff -r 23adc2138704 -r 04a05b2a7a36 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 10:39:52 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 26 10:57:04 2010 +0200
@@ -68,7 +68,7 @@
   val combtyp_of : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
   val combterm_from_term :
-    theory -> int -> (string * typ) list -> term -> combterm * typ list
+    theory -> (string * typ) list -> term -> combterm * typ list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val tfree_classes_of_terms : term list -> string list
   val tvar_classes_of_terms : term list -> string list
@@ -215,10 +215,9 @@
     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
 
 fun new_skolem_var_from_const s =
-  let
-    val ss = s |> space_explode Long_Name.separator
-    val n = length ss
-  in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
+  let val ss = s |> space_explode Long_Name.separator in
+    (nth ss (length ss - 2), 0)
+  end
 
 
 (**** Definitions and functions for FOL clauses for TPTP format output ****)
@@ -396,17 +395,18 @@
   | simple_combtype_of (TVar (x, _)) =
     CombTVar (make_schematic_type_var x, string_of_indexname x)
 
-fun new_skolem_const_name th_no s num_T_args =
-  [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
+fun new_skolem_const_name s num_T_args =
+  [new_skolem_const_prefix, s, string_of_int num_T_args]
   |> space_implode Long_Name.separator
 
-(* Converts a term (with combinators) into a combterm. Also accummulates sort
+(* Converts a term (with combinators) into a combterm. Also accumulates sort
    infomation. *)
-fun combterm_from_term thy th_no bs (P $ Q) =
-      let val (P', tsP) = combterm_from_term thy th_no bs P
-          val (Q', tsQ) = combterm_from_term thy th_no bs Q
-      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
-  | combterm_from_term thy _ _ (Const (c, T)) =
+fun combterm_from_term thy bs (P $ Q) =
+      let
+        val (P', tsP) = combterm_from_term thy bs P
+        val (Q', tsQ) = combterm_from_term thy bs Q
+      in (CombApp (P', Q'), union (op =) tsP tsQ) end
+  | combterm_from_term thy _ (Const (c, T)) =
       let
         val (tp, ts) = combtype_of T
         val tvar_list =
@@ -417,43 +417,42 @@
           |> map simple_combtype_of
         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
       in  (c',ts)  end
-  | combterm_from_term _ _ _ (Free (v, T)) =
+  | combterm_from_term _ _ (Free (v, T)) =
       let val (tp, ts) = combtype_of T
           val v' = CombConst (`make_fixed_var v, tp, [])
       in  (v',ts)  end
-  | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
+  | combterm_from_term _ _ (Var (v as (s, _), T)) =
     let
       val (tp, ts) = combtype_of T
       val v' =
         if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
           let
             val tys = T |> strip_type |> swap |> op ::
-            val s' = new_skolem_const_name th_no s (length tys)
+            val s' = new_skolem_const_name s (length tys)
           in
             CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
           end
         else
           CombVar ((make_schematic_var v, string_of_indexname v), tp)
     in (v', ts) end
-  | combterm_from_term _ _ bs (Bound j) =
+  | combterm_from_term _ bs (Bound j) =
       let
         val (s, T) = nth bs j
         val (tp, ts) = combtype_of T
         val v' = CombConst (`make_bound_var s, tp, [])
       in (v', ts) end
-  | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
+  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
-fun predicate_of thy th_no ((@{const Not} $ P), pos) =
-    predicate_of thy th_no (P, not pos)
-  | predicate_of thy th_no (t, pos) =
-    (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
+fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
+  | predicate_of thy (t, pos) =
+    (combterm_from_term thy [] (Envir.eta_contract t), pos)
 
-fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
-    literals_of_term1 args thy th_no P
-  | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
-    literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
-  | literals_of_term1 (lits, ts) thy th_no P =
-    let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
+fun literals_of_term1 args thy (@{const Trueprop} $ P) =
+    literals_of_term1 args thy P
+  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
+    literals_of_term1 (literals_of_term1 args thy P) thy Q
+  | literals_of_term1 (lits, ts) thy P =
+    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
       (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
     end
 val literals_of_term = literals_of_term1 ([], [])
@@ -607,9 +606,10 @@
             metis_lit pos "=" (map hol_term_to_fol_FT tms)
         | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
 
-fun literals_of_hol_term thy th_no mode t =
-      let val (lits, types_sorts) = literals_of_term thy th_no t
-      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
+fun literals_of_hol_term thy mode t =
+  let val (lits, types_sorts) = literals_of_term thy t in
+    (map (hol_literal_to_fol mode) lits, types_sorts)
+  end
 
 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
 fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
@@ -623,13 +623,13 @@
 fun metis_of_tfree tf =
   Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
 
-fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
+fun hol_thm_to_fol is_conjecture ctxt type_lits mode j old_skolems th =
   let
     val thy = ProofContext.theory_of ctxt
     val (old_skolems, (mlits, types_sorts)) =
      th |> prop_of |> Logic.strip_imp_concl
         |> conceal_old_skolem_terms j old_skolems
-        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
+        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   in
     if is_conjecture then
       (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
@@ -732,21 +732,20 @@
         | set_mode FT = FT
       val mode = set_mode mode0
       (*transform isabelle clause to metis clause *)
-      fun add_thm th_no is_conjecture (metis_ith, isa_ith)
+      fun add_thm is_conjecture (metis_ith, isa_ith)
                   {axioms, tfrees, old_skolems} : logic_map =
         let
           val (mth, tfree_lits, old_skolems) =
-            hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
+            hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
                            old_skolems metis_ith
         in
            {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
             tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
         end;
       val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
-                 |> fold (add_thm 0 true o `I) cls
+                 |> fold (add_thm true o `I) cls
                  |> add_tfrees
-                 |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
-                         (1 upto length thss ~~ thss)
+                 |> fold (fold (add_thm false o `I)) thss
       val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
       fun is_used c =
         exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -763,7 +762,7 @@
                                     []
                                   else
                                     thms)
-          in lmap |> fold (add_thm ~1 false) helper_ths end
+          in lmap |> fold (add_thm false) helper_ths end
   in
     (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
   end
diff -r 23adc2138704 -r 04a05b2a7a36 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 10:39:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Oct 26 10:57:04 2010 +0200
@@ -53,7 +53,7 @@
 
 fun combformula_for_prop thy =
   let
-    val do_term = combterm_from_term thy ~1
+    val do_term = combterm_from_term thy
     fun do_quant bs q s T t' =
       let val s = Name.variant (map fst bs) s in
         do_formula ((s, T) :: bs) t'