1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Fri Jul 01 15:53:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Fri Jul 01 15:53:38 2011 +0200
     1.3 @@ -13,10 +13,10 @@
     1.4    val full_typesN : string
     1.5    val partial_typesN : string
     1.6    val no_typesN : string
     1.7 -  val really_full_type_sys : string
     1.8 -  val full_type_sys : string
     1.9 -  val partial_type_sys : string
    1.10 -  val no_type_sys : string
    1.11 +  val really_full_type_enc : string
    1.12 +  val full_type_enc : string
    1.13 +  val partial_type_enc : string
    1.14 +  val no_type_enc : string
    1.15    val full_type_syss : string list
    1.16    val partial_type_syss : string list
    1.17    val trace : bool Config.T
    1.18 @@ -39,22 +39,22 @@
    1.19  val partial_typesN = "partial_types"
    1.20  val no_typesN = "no_types"
    1.21  
    1.22 -val really_full_type_sys = "poly_tags_heavy"
    1.23 -val full_type_sys = "poly_preds_heavy_query"
    1.24 -val partial_type_sys = "poly_args"
    1.25 -val no_type_sys = "erased"
    1.26 +val really_full_type_enc = "poly_tags_heavy"
    1.27 +val full_type_enc = "poly_preds_heavy_query"
    1.28 +val partial_type_enc = "poly_args"
    1.29 +val no_type_enc = "erased"
    1.30  
    1.31 -val full_type_syss = [full_type_sys, really_full_type_sys]
    1.32 -val partial_type_syss = partial_type_sys :: full_type_syss
    1.33 +val full_type_syss = [full_type_enc, really_full_type_enc]
    1.34 +val partial_type_syss = partial_type_enc :: full_type_syss
    1.35  
    1.36 -val type_sys_aliases =
    1.37 +val type_enc_aliases =
    1.38    [(full_typesN, full_type_syss),
    1.39     (partial_typesN, partial_type_syss),
    1.40 -   (no_typesN, [no_type_sys])]
    1.41 +   (no_typesN, [no_type_enc])]
    1.42  
    1.43 -fun method_call_for_type_sys type_syss =
    1.44 +fun method_call_for_type_enc type_syss =
    1.45    metisN ^ " (" ^
    1.46 -  (case AList.find (op =) type_sys_aliases type_syss of
    1.47 +  (case AList.find (op =) type_enc_aliases type_syss of
    1.48       [alias] => alias
    1.49     | _ => hd type_syss) ^ ")"
    1.50  
    1.51 @@ -102,7 +102,7 @@
    1.52  val resolution_params = {active = active_params, waiting = waiting_params}
    1.53  
    1.54  (* Main function to start Metis proof and reconstruction *)
    1.55 -fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
    1.56 +fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
    1.57    let val thy = Proof_Context.theory_of ctxt
    1.58        val new_skolemizer =
    1.59          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    1.60 @@ -118,7 +118,7 @@
    1.61        val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    1.62        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
    1.63        val (sym_tab, axioms, old_skolems) =
    1.64 -        prepare_metis_problem ctxt type_sys cls ths
    1.65 +        prepare_metis_problem ctxt type_enc cls ths
    1.66        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    1.67            reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
    1.68          | get_isa_thm _ (Isa_Raw ith) = ith
    1.69 @@ -126,7 +126,7 @@
    1.70        val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    1.71        val thms = axioms |> map fst
    1.72        val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    1.73 -      val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
    1.74 +      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
    1.75        val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    1.76    in
    1.77        case filter (fn t => prop_of t aconv @{prop False}) cls of
    1.78 @@ -186,7 +186,7 @@
    1.79           | _ =>
    1.80             (verbose_warning ctxt
    1.81                  ("Falling back on " ^
    1.82 -                 quote (method_call_for_type_sys fallback_type_syss) ^ "...");
    1.83 +                 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
    1.84              FOL_SOLVE fallback_type_syss ctxt cls ths0)
    1.85  
    1.86  val neg_clausify =
    1.87 @@ -249,7 +249,7 @@
    1.88  
    1.89  fun setup_method (binding, type_syss) =
    1.90    ((Args.parens (Scan.repeat Parse.short_ident)
    1.91 -    >> maps (fn s => case AList.lookup (op =) type_sys_aliases s of
    1.92 +    >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
    1.93                         SOME tss => tss
    1.94                       | NONE => [s]))
    1.95      |> Scan.option |> Scan.lift)