merged
authorhuffman
Mon Oct 11 07:09:42 2010 -0700 (2010-10-11)
changeset 39988a4b2971952f4
parent 39987 8c2f449af35a
parent 39980 f175e482dabe
child 39989 ad60d7311f43
merged
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sat Oct 09 07:24:49 2010 -0700
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Oct 11 07:09:42 2010 -0700
     1.3 @@ -1209,8 +1209,7 @@
     1.4  
     1.5    \item @{command "hide_class"}~@{text names} fully removes class
     1.6    declarations from a given name space; with the @{text "(open)"}
     1.7 -  option, only the base name is hidden.  Global (unqualified) names
     1.8 -  may never be hidden.
     1.9 +  option, only the base name is hidden.
    1.10  
    1.11    Note that hiding name space accesses has no impact on logical
    1.12    declarations --- they remain valid internally.  Entities that are no
     2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Oct 09 07:24:49 2010 -0700
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Oct 11 07:09:42 2010 -0700
     2.3 @@ -1252,8 +1252,7 @@
     2.4  
     2.5    \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
     2.6    declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
     2.7 -  option, only the base name is hidden.  Global (unqualified) names
     2.8 -  may never be hidden.
     2.9 +  option, only the base name is hidden.
    2.10  
    2.11    Note that hiding name space accesses has no impact on logical
    2.12    declarations --- they remain valid internally.  Entities that are no
     3.1 --- a/src/HOL/Metis.thy	Sat Oct 09 07:24:49 2010 -0700
     3.2 +++ b/src/HOL/Metis.thy	Mon Oct 11 07:09:42 2010 -0700
     3.3 @@ -29,7 +29,11 @@
     3.4  use "Tools/Metis/metis_translate.ML"
     3.5  use "Tools/Metis/metis_reconstruct.ML"
     3.6  use "Tools/Metis/metis_tactics.ML"
     3.7 -setup Metis_Tactics.setup
     3.8 +
     3.9 +setup {*
    3.10 +  Metis_Reconstruct.setup
    3.11 +  #> Metis_Tactics.setup
    3.12 +*}
    3.13  
    3.14  hide_const (open) fequal
    3.15  hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
     4.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Sat Oct 09 07:24:49 2010 -0700
     4.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Mon Oct 11 07:09:42 2010 -0700
     4.3 @@ -86,7 +86,7 @@
     4.4  
     4.5  lemma map_upds_distinct [simp]: 
     4.6    "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
     4.7 -apply (induct ys arbitrary: f vs rule: distinct.induct)
     4.8 +apply (induct ys arbitrary: f vs)
     4.9  apply simp
    4.10  apply (case_tac vs)
    4.11  apply simp_all
     5.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Oct 09 07:24:49 2010 -0700
     5.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Oct 11 07:09:42 2010 -0700
     5.3 @@ -8,7 +8,8 @@
     5.4  
     5.5  signature MESON =
     5.6  sig
     5.7 -  val trace: bool Unsynchronized.ref
     5.8 +  val trace : bool Config.T
     5.9 +  val max_clauses : int Config.T
    5.10    val term_pair_of: indexname * (typ * 'a) -> term * 'a
    5.11    val size_of_subgoals: thm -> int
    5.12    val has_too_many_clauses: Proof.context -> term -> bool
    5.13 @@ -39,17 +40,19 @@
    5.14    val make_meta_clause: thm -> thm
    5.15    val make_meta_clauses: thm list -> thm list
    5.16    val meson_tac: Proof.context -> thm list -> int -> tactic
    5.17 -  val setup: theory -> theory
    5.18 +  val setup : theory -> theory
    5.19  end
    5.20  
    5.21  structure Meson : MESON =
    5.22  struct
    5.23  
    5.24 -val trace = Unsynchronized.ref false;
    5.25 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    5.26 +val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false)
    5.27 +
    5.28 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    5.29  
    5.30 -val max_clauses_default = 60;
    5.31 -val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default);
    5.32 +val max_clauses_default = 60
    5.33 +val (max_clauses, max_clauses_setup) =
    5.34 +  Attrib.config_int "meson_max_clauses" (K max_clauses_default)
    5.35  
    5.36  (*No known example (on 1-5-2007) needs even thirty*)
    5.37  val iter_deepen_limit = 50;
    5.38 @@ -366,7 +369,7 @@
    5.39        and cnf_nil th = cnf_aux (th,[])
    5.40        val cls =
    5.41              if has_too_many_clauses ctxt (concl_of th)
    5.42 -            then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    5.43 +            then (trace_msg ctxt (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    5.44              else cnf_aux (th,ths)
    5.45    in  (cls, !ctxtr)  end;
    5.46  
    5.47 @@ -586,8 +589,8 @@
    5.48  (* "RS" can fail if "unify_search_bound" is too small. *)
    5.49  fun try_skolemize ctxt th =
    5.50    try (skolemize ctxt) th
    5.51 -  |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^
    5.52 -                                         Display.string_of_thm ctxt th)
    5.53 +  |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^
    5.54 +                                              Display.string_of_thm ctxt th)
    5.55             | _ => ())
    5.56  
    5.57  fun add_clauses th cls =
    5.58 @@ -678,7 +681,7 @@
    5.59      | goes =>
    5.60          let
    5.61            val horns = make_horns (cls @ ths)
    5.62 -          val _ = trace_msg (fn () =>
    5.63 +          val _ = trace_msg ctxt (fn () =>
    5.64              cat_lines ("meson method called:" ::
    5.65                map (Display.string_of_thm ctxt) (cls @ ths) @
    5.66                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    5.67 @@ -717,4 +720,8 @@
    5.68      name_thms "MClause#"
    5.69        (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    5.70  
    5.71 +val setup =
    5.72 +  trace_setup
    5.73 +  #> max_clauses_setup
    5.74 +
    5.75  end;
     6.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Oct 09 07:24:49 2010 -0700
     6.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Oct 11 07:09:42 2010 -0700
     6.3 @@ -11,7 +11,8 @@
     6.4  sig
     6.5    type mode = Metis_Translate.mode
     6.6  
     6.7 -  val trace : bool Unsynchronized.ref
     6.8 +  val trace : bool Config.T
     6.9 +  val trace_msg : Proof.context -> (unit -> string) -> unit
    6.10    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    6.11    val untyped_aconv : term -> term -> bool
    6.12    val replay_one_inference :
    6.13 @@ -20,6 +21,7 @@
    6.14      -> (Metis_Thm.thm * thm) list
    6.15    val discharge_skolem_premises :
    6.16      Proof.context -> (thm * term) option list -> thm -> thm
    6.17 +  val setup : theory -> theory
    6.18  end;
    6.19  
    6.20  structure Metis_Reconstruct : METIS_RECONSTRUCT =
    6.21 @@ -27,8 +29,9 @@
    6.22  
    6.23  open Metis_Translate
    6.24  
    6.25 -val trace = Unsynchronized.ref false
    6.26 -fun trace_msg msg = if !trace then tracing (msg ()) else ()
    6.27 +val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
    6.28 +
    6.29 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    6.30  
    6.31  datatype term_or_type = SomeTerm of term | SomeType of typ
    6.32  
    6.33 @@ -92,8 +95,8 @@
    6.34  (*Maps metis terms to isabelle terms*)
    6.35  fun hol_term_from_metis_PT ctxt fol_tm =
    6.36    let val thy = ProofContext.theory_of ctxt
    6.37 -      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
    6.38 -                                  Metis_Term.toString fol_tm)
    6.39 +      val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
    6.40 +                                       Metis_Term.toString fol_tm)
    6.41        fun tm_to_tt (Metis_Term.Var v) =
    6.42               (case strip_prefix_and_unascii tvar_prefix v of
    6.43                    SOME w => SomeType (make_tvar w)
    6.44 @@ -160,8 +163,8 @@
    6.45  
    6.46  (*Maps fully-typed metis terms to isabelle terms*)
    6.47  fun hol_term_from_metis_FT ctxt fol_tm =
    6.48 -  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
    6.49 -                                  Metis_Term.toString fol_tm)
    6.50 +  let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
    6.51 +                                       Metis_Term.toString fol_tm)
    6.52        fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
    6.53               (case strip_prefix_and_unascii schematic_var_prefix v of
    6.54                    SOME w =>  mk_var(w, dummyT)
    6.55 @@ -188,10 +191,12 @@
    6.56                | NONE => (*Not a constant. Is it a fixed variable??*)
    6.57              case strip_prefix_and_unascii fixed_var_prefix x of
    6.58                  SOME v => Free (v, dummyT)
    6.59 -              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
    6.60 -                  hol_term_from_metis_PT ctxt t))
    6.61 -        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
    6.62 -            hol_term_from_metis_PT ctxt t)
    6.63 +              | NONE => (trace_msg ctxt (fn () =>
    6.64 +                                      "hol_term_from_metis_FT bad const: " ^ x);
    6.65 +                         hol_term_from_metis_PT ctxt t))
    6.66 +        | cvt t = (trace_msg ctxt (fn () =>
    6.67 +                   "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
    6.68 +                   hol_term_from_metis_PT ctxt t)
    6.69    in fol_tm |> cvt end
    6.70  
    6.71  fun hol_term_from_metis FT = hol_term_from_metis_FT
    6.72 @@ -199,11 +204,12 @@
    6.73  
    6.74  fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
    6.75    let val ts = map (hol_term_from_metis mode ctxt) fol_tms
    6.76 -      val _ = trace_msg (fn () => "  calling type inference:")
    6.77 -      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
    6.78 +      val _ = trace_msg ctxt (fn () => "  calling type inference:")
    6.79 +      val _ = app (fn t => trace_msg ctxt
    6.80 +                                     (fn () => Syntax.string_of_term ctxt t)) ts
    6.81        val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
    6.82                     |> infer_types ctxt
    6.83 -      val _ = app (fn t => trace_msg
    6.84 +      val _ = app (fn t => trace_msg ctxt
    6.85                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    6.86                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
    6.87                    ts'
    6.88 @@ -215,10 +221,10 @@
    6.89  
    6.90  (*for debugging only*)
    6.91  (*
    6.92 -fun print_thpair (fth,th) =
    6.93 -  (trace_msg (fn () => "=============================================");
    6.94 -   trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
    6.95 -   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    6.96 +fun print_thpair ctxt (fth,th) =
    6.97 +  (trace_msg ctxt (fn () => "=============================================");
    6.98 +   trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
    6.99 +   trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   6.100  *)
   6.101  
   6.102  fun lookth thpairs (fth : Metis_Thm.thm) =
   6.103 @@ -264,12 +270,12 @@
   6.104              val t = hol_term_from_metis mode ctxt y
   6.105          in  SOME (cterm_of thy (Var v), t)  end
   6.106          handle Option.Option =>
   6.107 -               (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
   6.108 -                                    " in " ^ Display.string_of_thm ctxt i_th);
   6.109 +               (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
   6.110 +                                         " in " ^ Display.string_of_thm ctxt i_th);
   6.111                  NONE)
   6.112               | TYPE _ =>
   6.113 -               (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   6.114 -                                    " in " ^ Display.string_of_thm ctxt i_th);
   6.115 +               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   6.116 +                                         " in " ^ Display.string_of_thm ctxt i_th);
   6.117                  NONE)
   6.118        fun remove_typeinst (a, t) =
   6.119              case strip_prefix_and_unascii schematic_var_prefix a of
   6.120 @@ -277,14 +283,14 @@
   6.121                | NONE => case strip_prefix_and_unascii tvar_prefix a of
   6.122                  SOME _ => NONE          (*type instantiations are forbidden!*)
   6.123                | NONE => SOME (a,t)    (*internal Metis var?*)
   6.124 -      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   6.125 +      val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   6.126        val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   6.127        val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   6.128        val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
   6.129                         |> infer_types ctxt
   6.130        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   6.131        val substs' = ListPair.zip (vars, map ctm_of tms)
   6.132 -      val _ = trace_msg (fn () =>
   6.133 +      val _ = trace_msg ctxt (fn () =>
   6.134          cat_lines ("subst_translations:" ::
   6.135            (substs' |> map (fn (x, y) =>
   6.136              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   6.137 @@ -375,8 +381,8 @@
   6.138    let
   6.139      val thy = ProofContext.theory_of ctxt
   6.140      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   6.141 -    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   6.142 -    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   6.143 +    val _ = trace_msg ctxt (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   6.144 +    val _ = trace_msg ctxt (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   6.145    in
   6.146      (* Trivial cases where one operand is type info *)
   6.147      if Thm.eq_thm (TrueI, i_th1) then
   6.148 @@ -387,15 +393,15 @@
   6.149        let
   6.150          val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
   6.151                                (Metis_Term.Fn atm)
   6.152 -        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   6.153 +        val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   6.154          val prems_th1 = prems_of i_th1
   6.155          val prems_th2 = prems_of i_th2
   6.156          val index_th1 = literal_index (mk_not i_atm) prems_th1
   6.157                handle Empty => raise Fail "Failed to find literal in th1"
   6.158 -        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   6.159 +        val _ = trace_msg ctxt (fn () => "  index_th1: " ^ Int.toString index_th1)
   6.160          val index_th2 = literal_index i_atm prems_th2
   6.161                handle Empty => raise Fail "Failed to find literal in th2"
   6.162 -        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   6.163 +        val _ = trace_msg ctxt (fn () => "  index_th2: " ^ Int.toString index_th2)
   6.164      in
   6.165        resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
   6.166      end
   6.167 @@ -411,7 +417,7 @@
   6.168  fun refl_inf ctxt mode old_skolems t =
   6.169    let val thy = ProofContext.theory_of ctxt
   6.170        val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
   6.171 -      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   6.172 +      val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   6.173        val c_t = cterm_incr_types thy refl_idx i_t
   6.174    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   6.175  
   6.176 @@ -430,7 +436,7 @@
   6.177    let val thy = ProofContext.theory_of ctxt
   6.178        val m_tm = Metis_Term.Fn atm
   6.179        val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
   6.180 -      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   6.181 +      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   6.182        fun replace_item_list lx 0 (_::ls) = lx::ls
   6.183          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   6.184        fun path_finder_FO tm [] = (tm, Bound 0)
   6.185 @@ -444,7 +450,7 @@
   6.186                                  "equality_inf: " ^ Int.toString p ^ " adj " ^
   6.187                                  Int.toString adjustment ^ " term " ^
   6.188                                  Syntax.string_of_term ctxt tm)
   6.189 -                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   6.190 +                val _ = trace_msg ctxt (fn () => "path_finder: " ^ Int.toString p ^
   6.191                                        "  " ^ Syntax.string_of_term ctxt tm_p)
   6.192                  val (r,t) = path_finder_FO tm_p ps
   6.193              in
   6.194 @@ -496,12 +502,12 @@
   6.195          | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   6.196        val (tm_subst, body) = path_finder_lit i_atm fp
   6.197        val tm_abs = Abs ("x", type_of tm_subst, body)
   6.198 -      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   6.199 -      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   6.200 -      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   6.201 +      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   6.202 +      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   6.203 +      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   6.204        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   6.205        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   6.206 -      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   6.207 +      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   6.208        val eq_terms = map (pairself (cterm_of thy))
   6.209          (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   6.210    in  cterm_instantiate eq_terms subst'  end;
   6.211 @@ -540,13 +546,13 @@
   6.212  
   6.213  fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
   6.214    let
   6.215 -    val _ = trace_msg (fn () => "=============================================")
   6.216 -    val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   6.217 -    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   6.218 +    val _ = trace_msg ctxt (fn () => "=============================================")
   6.219 +    val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   6.220 +    val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   6.221      val th = step ctxt mode old_skolems thpairs (fol_th, inf)
   6.222               |> flexflex_first_order
   6.223 -    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   6.224 -    val _ = trace_msg (fn () => "=============================================")
   6.225 +    val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   6.226 +    val _ = trace_msg ctxt (fn () => "=============================================")
   6.227      val num_metis_lits =
   6.228        fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
   6.229               |> count is_metis_literal_genuine
   6.230 @@ -556,8 +562,6 @@
   6.231              else error "Cannot replay Metis proof in Isabelle: Out of sync."
   6.232    in (fol_th, th) :: thpairs end
   6.233  
   6.234 -(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *)
   6.235 -
   6.236  fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
   6.237  
   6.238  (* In principle, it should be sufficient to apply "assume_tac" to unify the
   6.239 @@ -790,8 +794,10 @@
   6.240                THEN ALLGOALS (fn i =>
   6.241                         rtac @{thm Meson.skolem_COMBK_I} i
   6.242                         THEN rotate_tac (rotation_for_subgoal i) i
   6.243 -                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   6.244 +(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*)
   6.245                         THEN assume_tac i)))
   6.246      end
   6.247  
   6.248 +val setup = trace_setup
   6.249 +
   6.250  end;
     7.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Sat Oct 09 07:24:49 2010 -0700
     7.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 11 07:09:42 2010 -0700
     7.3 @@ -9,7 +9,7 @@
     7.4  
     7.5  signature METIS_TACTICS =
     7.6  sig
     7.7 -  val trace : bool Unsynchronized.ref
     7.8 +  val trace : bool Config.T
     7.9    val type_lits : bool Config.T
    7.10    val new_skolemizer : bool Config.T
    7.11    val metis_tac : Proof.context -> thm list -> int -> tactic
    7.12 @@ -24,8 +24,6 @@
    7.13  open Metis_Translate
    7.14  open Metis_Reconstruct
    7.15  
    7.16 -fun trace_msg msg = if !trace then tracing (msg ()) else ()
    7.17 -
    7.18  val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
    7.19  val (new_skolemizer, new_skolemizer_setup) =
    7.20    Attrib.config_bool "metis_new_skolemizer" (K false)
    7.21 @@ -67,21 +65,21 @@
    7.22               (0 upto length ths0 - 1) ths0
    7.23        val thss = map (snd o snd) th_cls_pairs
    7.24        val dischargers = map (fst o snd) th_cls_pairs
    7.25 -      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    7.26 -      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
    7.27 -      val _ = trace_msg (fn () => "THEOREM CLAUSES")
    7.28 -      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
    7.29 +      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    7.30 +      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    7.31 +      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    7.32 +      val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss
    7.33        val (mode, {axioms, tfrees, old_skolems}) =
    7.34          build_logic_map mode ctxt type_lits cls thss
    7.35        val _ = if null tfrees then ()
    7.36 -              else (trace_msg (fn () => "TFREE CLAUSES");
    7.37 +              else (trace_msg ctxt (fn () => "TFREE CLAUSES");
    7.38                      app (fn TyLitFree ((s, _), (s', _)) =>
    7.39 -                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
    7.40 -      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
    7.41 +                            trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
    7.42 +      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    7.43        val thms = map #1 axioms
    7.44 -      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
    7.45 -      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
    7.46 -      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
    7.47 +      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    7.48 +      val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
    7.49 +      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    7.50    in
    7.51        case filter (is_false o prop_of) cls of
    7.52            false_th::_ => [false_th RS @{thm FalseE}]
    7.53 @@ -89,7 +87,7 @@
    7.54        case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
    7.55             |> Metis_Resolution.loop of
    7.56            Metis_Resolution.Contradiction mth =>
    7.57 -            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
    7.58 +            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
    7.59                            Metis_Thm.toString mth)
    7.60                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
    7.61                               (*add constraints arising from converting goal to clause form*)
    7.62 @@ -97,8 +95,8 @@
    7.63                  val result =
    7.64                    fold (replay_one_inference ctxt' mode old_skolems) proof axioms
    7.65                  and used = map_filter (used_axioms axioms) proof
    7.66 -                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
    7.67 -                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
    7.68 +                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    7.69 +                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    7.70                  val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
    7.71                    if have_common_thm used cls then NONE else SOME name)
    7.72              in
    7.73 @@ -113,12 +111,12 @@
    7.74                    ();
    7.75                  case result of
    7.76                      (_,ith)::_ =>
    7.77 -                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
    7.78 +                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
    7.79                           [discharge_skolem_premises ctxt dischargers ith])
    7.80 -                  | _ => (trace_msg (fn () => "Metis: No result"); [])
    7.81 +                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
    7.82              end
    7.83          | Metis_Resolution.Satisfiable _ =>
    7.84 -            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
    7.85 +            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
    7.86               [])
    7.87    end;
    7.88  
    7.89 @@ -150,7 +148,7 @@
    7.90  
    7.91  fun generic_metis_tac mode ctxt ths i st0 =
    7.92    let
    7.93 -    val _ = trace_msg (fn () =>
    7.94 +    val _ = trace_msg ctxt (fn () =>
    7.95          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
    7.96    in
    7.97      if exists_type type_has_top_sort (prop_of st0) then
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Sat Oct 09 07:24:49 2010 -0700
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Oct 11 07:09:42 2010 -0700
     8.3 @@ -13,10 +13,6 @@
     8.4  
     8.5    val axiom_prefix : string
     8.6    val conjecture_prefix : string
     8.7 -  val helper_prefix : string
     8.8 -  val class_rel_clause_prefix : string
     8.9 -  val arity_clause_prefix : string
    8.10 -  val tfrees_name : string
    8.11    val prepare_axiom :
    8.12      Proof.context -> (string * 'a) * thm
    8.13      -> term * ((string * 'a) * fol_formula) option
    8.14 @@ -38,7 +34,7 @@
    8.15  val helper_prefix = "help_"
    8.16  val class_rel_clause_prefix = "clrel_";
    8.17  val arity_clause_prefix = "arity_"
    8.18 -val tfrees_name = "tfrees"
    8.19 +val tfree_prefix = "tfree_"
    8.20  
    8.21  (* Freshness almost guaranteed! *)
    8.22  val sledgehammer_weak_prefix = "Sledgehammer:"
    8.23 @@ -363,13 +359,13 @@
    8.24  fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
    8.25    map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
    8.26  
    8.27 -fun problem_line_for_free_type lit =
    8.28 -  Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
    8.29 +fun problem_line_for_free_type j lit =
    8.30 +  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
    8.31  fun problem_lines_for_free_types conjectures =
    8.32    let
    8.33      val litss = map free_type_literals_for_conjecture conjectures
    8.34      val lits = fold (union (op =)) litss []
    8.35 -  in map problem_line_for_free_type lits end
    8.36 +  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
    8.37  
    8.38  (** "hBOOL" and "hAPP" **)
    8.39