# HG changeset patch
# User blanchet
# Date 1304542593 -7200
# Node ID 2123b2608b14def059da993d63dc6c5ee7433bce
# Parent  e60326e7ee95dee1c108487e51f80fd36e56876c
renamed "many_typed" to "simple" (as in simple types)

diff -r e60326e7ee95 -r 2123b2608b14 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 04 22:54:10 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 04 22:56:33 2011 +0200
@@ -378,14 +378,14 @@
 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
 val remote_tofof_e =
   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Conjecture [Tff] (K 200 (* FUDGE *)) ["many_typed"]
+             Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
                      (#best_type_systems e_config)
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
-             (K 250 (* FUDGE *)) ["many_typed"]
+             (K 250 (* FUDGE *)) ["simple"]
 
 (* Setup *)
 
diff -r e60326e7ee95 -r 2123b2608b14 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 22:54:10 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 22:56:33 2011 +0200
@@ -17,7 +17,7 @@
     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
 
   datatype type_system =
-    Many_Typed of type_level |
+    Simple of type_level |
     Preds of polymorphism * type_level |
     Tags of polymorphism * type_level
 
@@ -96,7 +96,7 @@
   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
 
 datatype type_system =
-  Many_Typed of type_level |
+  Simple of type_level |
   Preds of polymorphism * type_level |
   Tags of polymorphism * type_level
 
@@ -116,7 +116,7 @@
             | NONE => (All_Types, s))
   |> (fn (polymorphism, (level, core)) =>
          case (core, (polymorphism, level)) of
-           ("many_typed", (Polymorphic (* naja *), level)) => Many_Typed level
+           ("simple", (Polymorphic (* naja *), level)) => Simple level
          | ("preds", extra) => Preds extra
          | ("tags", extra) => Tags extra
          | ("args", (_, All_Types (* naja *))) =>
@@ -125,11 +125,11 @@
            Preds (polymorphism, No_Types)
          | _ => error ("Unknown type system: " ^ quote s ^ "."))
 
-fun polymorphism_of_type_sys (Many_Typed _) = Mangled_Monomorphic
+fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic
   | polymorphism_of_type_sys (Preds (poly, _)) = poly
   | polymorphism_of_type_sys (Tags (poly, _)) = poly
 
-fun level_of_type_sys (Many_Typed level) = level
+fun level_of_type_sys (Simple level) = level
   | level_of_type_sys (Preds (_, level)) = level
   | level_of_type_sys (Tags (_, level)) = level
 
@@ -783,7 +783,7 @@
       end
     val do_bound_type =
       case type_sys of
-        Many_Typed level =>
+        Simple level =>
         SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
       | _ => K NONE
     fun do_out_of_bound_type (s, T) =
@@ -886,7 +886,7 @@
 fun should_declare_sym type_sys pred_sym s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   not (String.isPrefix "$" s) andalso
-  ((case type_sys of Many_Typed _ => true | _ => false) orelse not pred_sym)
+  ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
 
 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
   let
@@ -980,7 +980,7 @@
 
 fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) =
   case type_sys of
-    Many_Typed _ => map (decl_line_for_sym s) decls
+    Simple _ => map (decl_line_for_sym s) decls
   | _ =>
     let
       val decls =
@@ -1077,7 +1077,7 @@
     val problem =
       problem
       |> (case type_sys of
-            Many_Typed _ =>
+            Simple _ =>
             cons (type_declsN,
                   map decl_line_for_tff_type (tff_types_in_problem problem))
           | _ => I)
diff -r e60326e7ee95 -r 2123b2608b14 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 04 22:54:10 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 04 22:56:33 2011 +0200
@@ -346,14 +346,14 @@
 val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
-  [Preds (Polymorphic, Const_Arg_Types), Many_Typed All_Types]
+  [Preds (Polymorphic, Const_Arg_Types), Simple All_Types]
 
-fun adjust_dumb_type_sys formats (Many_Typed level) =
-    if member (op =) formats Tff then (Tff, Many_Typed level)
+fun adjust_dumb_type_sys formats (Simple level) =
+    if member (op =) formats Tff then (Tff, Simple level)
     else (Fof, Preds (Mangled_Monomorphic, level))
   | adjust_dumb_type_sys formats type_sys =
     if member (op =) formats Fof then (Fof, type_sys)
-    else (Tff, Many_Typed (level_of_type_sys type_sys))
+    else (Tff, Simple (level_of_type_sys type_sys))
 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
     adjust_dumb_type_sys formats type_sys
   | determine_format_and_type_sys best_type_systems formats