# HG changeset patch
# User blanchet
# Date 1332247989 -3600
# Node ID 62ca06cc5a999d44116ccbe3ebeaf3a9e841cff6
# Parent  631adf003bb0963682dc5ce394fb349dd37a7669
remove two options that were found to play hardly any role

diff -r 631adf003bb0 -r 62ca06cc5a99 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 20 13:53:09 2012 +0100
@@ -30,8 +30,6 @@
     No_Types
   type type_enc
 
-  val type_tag_idempotence : bool Config.T
-  val type_tag_arguments : bool Config.T
   val no_lamsN : string
   val hide_lamsN : string
   val liftingN : string
@@ -67,7 +65,6 @@
   val lam_fact_prefix : string
   val typed_helper_suffix : string
   val untyped_helper_suffix : string
-  val type_tag_idempotence_helper_name : string
   val predicator_name : string
   val app_op_name : string
   val type_guard_name : string
@@ -119,11 +116,6 @@
 
 type name = string * string
 
-val type_tag_idempotence =
-  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
-val type_tag_arguments =
-  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
-
 val no_lamsN = "no_lams" (* used internally; undocumented *)
 val hide_lamsN = "hide_lams"
 val liftingN = "lifting"
@@ -178,7 +170,6 @@
 val lam_fact_prefix = "ATP.lambda_"
 val typed_helper_suffix = "_T"
 val untyped_helper_suffix = "_U"
-val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
 
 val predicator_name = "pp"
 val app_op_name = "aa"
@@ -1671,17 +1662,6 @@
 
 val type_tag = `(make_fixed_const NONE) type_tag_name
 
-fun type_tag_idempotence_fact type_enc =
-  let
-    fun var s = ATerm (`I s, [])
-    fun tag tm = ATerm (type_tag, [var "A", tm])
-    val tagged_var = tag (var "X")
-  in
-    Formula (type_tag_idempotence_helper_name, Axiom,
-             eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
-             NONE, isabelle_info spec_eqN helper_rank)
-  end
-
 fun should_specialize_helper type_enc t =
   polymorphism_of_type_enc type_enc <> Polymorphic andalso
   level_of_type_enc type_enc <> No_Types andalso
@@ -2361,25 +2341,7 @@
         end
       else
         I
-    fun add_formula_for_arg k =
-      let val arg_T = nth arg_Ts k in
-        if should_encode arg_T then
-          case chop k bounds of
-            (bounds1, bound :: bounds2) =>
-            cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
-                           eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
-                              (cst bounds),
-                           NONE, isabelle_info spec_eqN helper_rank))
-          | _ => raise Fail "expected nonempty tail"
-        else
-          I
-      end
-  in
-    [] |> not pred_sym ? add_formula_for_res
-       |> (Config.get ctxt type_tag_arguments andalso
-           grain = Positively_Naked_Vars)
-          ? fold add_formula_for_arg (ary - 1 downto 0)
-  end
+  in [] |> not pred_sym ? add_formula_for_res end
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
@@ -2506,12 +2468,6 @@
             o uncurried_alias_lines_for_sym ctxt monom_constrs format
                   conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
 
-fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
-    Config.get ctxt type_tag_idempotence andalso
-    is_type_level_monotonicity_based level andalso
-    poly <> Mangled_Monomorphic
-  | needs_type_tag_idempotence _ _ = false
-
 val implicit_declsN = "Should-be-implicit typings"
 val explicit_declsN = "Explicit typings"
 val uncurried_alias_eqsN = "Uncurried aliases"
@@ -2659,10 +2615,6 @@
       0 upto length helpers - 1 ~~ helpers
       |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
                                     false true mono type_enc (K default_rank))
-      |> (if needs_type_tag_idempotence ctxt type_enc then
-            cons (type_tag_idempotence_fact type_enc)
-          else
-            I)
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        FLOTTER hack. *)
     val problem =
diff -r 631adf003bb0 -r 62ca06cc5a99 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 13:53:09 2012 +0100
@@ -168,8 +168,7 @@
                   |> Metis_LiteralSet.fromList
                   |> Metis_Thm.axiom, isa)
     in
-      if ident = type_tag_idempotence_helper_name orelse
-         String.isPrefix tags_sym_formula_prefix ident then
+      if String.isPrefix tags_sym_formula_prefix ident then
         Isa_Reflexive_or_Trivial |> some
       else if String.isPrefix conjecture_prefix ident then
         NONE