merged

--- a/src/HOL/Code_Evaluation.thy	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Wed Dec 09 11:53:51 2009 +0100
@@ -279,7 +279,7 @@
 val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
 
 fun eval_term thy t =
-  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+  Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end;
 *}

--- a/src/HOL/GCD.thy	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/GCD.thy	Wed Dec 09 11:53:51 2009 +0100
@@ -25,7 +25,7 @@
 *)
 
 
-header {* GCD *}
+header {* Greates common divisor and least common multiple *}
 
 theory GCD
 imports Fact Parity
@@ -33,7 +33,7 @@
 
 declare One_nat_def [simp del]
 
-subsection {* gcd *}
+subsection {* GCD and LCM definitions *}
 
 class gcd = zero + one + dvd +
 
@@ -50,11 +50,7 @@
 
 end
 
-
-(* definitions for the natural numbers *)
-
 instantiation nat :: gcd
-
 begin
 
 fun
@@ -72,11 +68,7 @@
 
 end
 
-
-(* definitions for the integers *)
-
 instantiation int :: gcd
-
 begin
 
 definition
@@ -94,8 +86,7 @@
 end
 
 
-subsection {* Set up Transfer *}
-
+subsection {* Transfer setup *}
 
 lemma transfer_nat_int_gcd:
   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
@@ -125,7 +116,7 @@
     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
 
 
-subsection {* GCD *}
+subsection {* GCD properties *}
 
 (* was gcd_induct *)
 lemma gcd_nat_induct:
@@ -547,6 +538,10 @@
 apply simp
 done
 
+lemma gcd_code_int [code]:
+  "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
+
 
 subsection {* Coprimality *}
 
@@ -1225,9 +1220,9 @@
 qed
 
 
-subsection {* LCM *}
+subsection {* LCM properties *}
 
-lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
+lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
   by (simp add: lcm_int_def lcm_nat_def zdiv_int
     zmult_int [symmetric] gcd_int_def)
 
@@ -1443,6 +1438,7 @@
 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
 by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
 
+
 subsubsection {* The complete divisibility lattice *}
 
 

--- a/src/HOL/HOL.thy	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 09 11:53:51 2009 +0100
@@ -1971,7 +1971,7 @@
     val t = Thm.term_of ct;
     val dummy = @{cprop True};
   in case try HOLogic.dest_Trueprop t
-   of SOME t' => if Code_ML.eval NONE
+   of SOME t' => if Code_Eval.eval NONE
          ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
        then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
        else dummy

--- a/src/HOL/IsaMakefile	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 09 11:53:51 2009 +0100
@@ -103,6 +103,7 @@
   $(SRC)/Provers/hypsubst.ML \
   $(SRC)/Provers/quantifier1.ML \
   $(SRC)/Provers/splitter.ML \
+  $(SRC)/Tools/Code/code_eval.ML \
   $(SRC)/Tools/Code/code_haskell.ML \
   $(SRC)/Tools/Code/code_ml.ML \
   $(SRC)/Tools/Code/code_preproc.ML \

--- a/src/HOL/Library/Eval_Witness.thy	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Dec 09 11:53:51 2009 +0100
@@ -68,7 +68,7 @@
     | dest_exs _ _ = sys_error "dest_exs";
   val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
-  if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
+  if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
   then Thm.cterm_of thy goal
   else @{cprop True} (*dummy*)
 end

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -20,6 +20,7 @@
   type run_action = int -> run_args -> unit
   type action = init_action * run_action * done_action
   val catch : (int -> string) -> run_action -> run_action
+  val app_timeout : (int -> string) -> run_action -> run_action -> run_action
   val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
@@ -72,9 +73,18 @@
 fun app_with f g x = (g x; ())
   handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
 
+fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
+
 fun catch tag f id (st as {log, ...}: run_args) =
-  let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
-  in app_with log_exn (f id) st end
+  app_with (log_exn log tag id) (f id) st
+
+fun app_timeout tag f g id (st as {log, ...}: run_args) =
+  let
+    val continue = (f id st; true)
+      handle (exn as Exn.Interrupt) => reraise exn
+           | (exn as TimeLimit.TimeOut) => (log_exn log tag id exn; false)
+           | _ => true
+  in if continue then g id st else () end
 
 fun register (init, run, done) thy =
   let val id = length (Actions.get thy) + 1

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -12,6 +12,7 @@
 val full_typesK = "full_types"
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
+val metis_ftK = "metis_ft"
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -45,11 +46,6 @@
   it_ratios: int
   }
 
-(* The first me_data component is only used if "minimize" is on.
-   Then it records how metis behaves with un-minimized lemmas.
-*)
-datatype data = Data of sh_data * me_data * min_data * me_data
-
 fun make_sh_data
       (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) =
   ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
@@ -62,28 +58,63 @@
   MeData{calls=calls, success=success, proofs=proofs, time=time,
          timeout=timeout, lemmas=lemmas, posns=posns}
 
-val empty_data =
-  Data(make_sh_data (0, 0, 0, 0, 0, 0, 0),
-       make_me_data(0, 0, 0, 0, 0, (0,0,0), []),
-       MinData{succs=0, ab_ratios=0, it_ratios=0},
-       make_me_data(0, 0, 0, 0, 0, (0,0,0), []))
+val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0)
+val empty_min_data = make_min_data(0, 0, 0)
+val empty_me_data = make_me_data(0, 0, 0, 0, 0, (0,0,0), [])
+
+fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa,
+  time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
+  time_atp, time_atp_fail)
+
+fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
+  (succs, ab_ratios, it_ratios)
+
+fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
+  posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
+
+
+datatype metis = Unminimized | Minimized | UnminimizedFT | MinimizedFT
+
+datatype data = Data of {
+  sh: sh_data,
+  min: min_data,
+  me_u: me_data, (* metis with unminimized set of lemmas *)
+  me_m: me_data, (* metis with minimized set of lemmas *)
+  me_uft: me_data, (* metis with unminimized set of lemmas and fully-typed *)
+  me_mft: me_data, (* metis with minimized set of lemmas and fully-typed *)
+  mini: bool   (* with minimization *)
+  }
 
-fun map_sh_data f
-    (Data(ShData{calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail},
-          meda0, minda, meda)) =
-  Data (make_sh_data (f (calls,success,lemmas,max_lems,
-                         time_isa,time_atp,time_atp_fail)),
-        meda0, minda, meda)
+fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) =
+  Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft,
+    mini=mini}
+
+val empty_data = make_data (empty_sh_data, empty_min_data,
+  empty_me_data, empty_me_data, empty_me_data, empty_me_data, false)
+
+fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+  let val sh' = make_sh_data (f (tuple_of_sh_data sh))
+  in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end
+
+fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+  let val min' = make_min_data (f (tuple_of_min_data min))
+  in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end
 
-fun map_min_data f
-  (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) =
-  Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda)
+fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+  let
+    fun map_me g Unminimized   (u, m, uft, mft) = (g u, m, uft, mft)
+      | map_me g Minimized     (u, m, uft, mft) = (u, g m, uft, mft)
+      | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
+      | map_me g MinimizedFT   (u, m, uft, mft) = (u, m, uft, g mft)
 
-fun map_me_data0 f (Data (shda, MeData{calls,success,proofs,time,timeout,lemmas,posns}, minda, meda)) =
-  Data(shda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)), minda, meda)
+    val f' = make_me_data o f o tuple_of_me_data
 
-fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,proofs,time,timeout,lemmas,posns})) =
-  Data(shda, meda0, minda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)))
+    val (me_u', me_m', me_uft', me_mft') =
+      map_me f' m (me_u, me_m, me_uft, me_mft)
+  in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end
+
+fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) =
+  make_data (sh, min, me_u, me_m, me_uft, me_mft, mini)
 
 fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
 
@@ -136,49 +167,21 @@
   (fn (calls,success,proofs,time,timeout,lemmas,posns)
     => (calls, success, proofs + 1, time, timeout, lemmas,posns))
 
-fun inc_metis_time t = map_me_data
+fun inc_metis_time m t = map_me_data
  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-  => (calls, success, proofs, time + t, timeout, lemmas,posns))
+  => (calls, success, proofs, time + t, timeout, lemmas,posns)) m
 
 val inc_metis_timeout = map_me_data
   (fn (calls,success,proofs,time,timeout,lemmas,posns)
     => (calls, success, proofs, time, timeout + 1, lemmas,posns))
 
-fun inc_metis_lemmas n = map_me_data
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs, time, timeout, inc_max n lemmas, posns))
-
-fun inc_metis_posns pos = map_me_data
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs, time, timeout, lemmas, pos::posns))
-
-val inc_metis_calls0 = map_me_data0 
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls + 1, success, proofs, time, timeout, lemmas,posns))
-
-val inc_metis_success0 = map_me_data0
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success + 1, proofs, time, timeout, lemmas,posns))
-
-val inc_metis_proofs0 = map_me_data0
+fun inc_metis_lemmas m n = map_me_data
   (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs + 1, time, timeout, lemmas,posns))
+    => (calls, success, proofs, time, timeout, inc_max n lemmas, posns)) m
 
-fun inc_metis_time0 t = map_me_data0
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs, time + t, timeout, lemmas,posns))
-
-val inc_metis_timeout0 = map_me_data0
+fun inc_metis_posns m pos = map_me_data
   (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs, time, timeout + 1, lemmas,posns))
-
-fun inc_metis_lemmas0 n = map_me_data0
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs, time, timeout, inc_max n lemmas, posns))
-
-fun inc_metis_posns0 pos = map_me_data0
-  (fn (calls,success,proofs,time,timeout,lemmas,posns)
-    => (calls, success, proofs, time, timeout, lemmas, pos::posns))
+    => (calls, success, proofs, time, timeout, lemmas, pos::posns)) m
 
 local
 
@@ -189,7 +192,8 @@
 fun avg_time t n =
   if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
 
-fun log_sh_data log calls success lemmas max_lems time_isa time_atp time_atp_fail =
+fun log_sh_data log
+    (calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) =
  (log ("Total number of sledgehammer calls: " ^ str calls);
   log ("Number of successful sledgehammer calls: " ^ str success);
   log ("Number of sledgehammer lemmas: " ^ str lemmas);
@@ -211,8 +215,9 @@
   let val str0 = string_of_int o the_default 0
   in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
 
-fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time
-    metis_timeout (lemmas, lems_sos, lems_max) metis_posns =
+fun log_me_data log tag sh_calls (metis_calls, metis_success,
+    metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
+    metis_posns) =
  (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
   log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
     " (proof: " ^ str metis_proofs ^ ")");
@@ -222,14 +227,14 @@
   log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos);
   log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max);
   log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time));
-  log ("Average time for successful metis calls: " ^
+  log ("Average time for successful " ^ tag ^ "metis calls: " ^
     str3 (avg_time metis_time metis_success));
   if tag=""
   then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
   else ()
  )
 
-fun log_min_data log succs ab_ratios it_ratios =
+fun log_min_data log (succs, ab_ratios, it_ratios) =
   (log ("Number of successful minimizations: " ^ string_of_int succs);
    log ("After/before ratios: " ^ string_of_int ab_ratios);
    log ("Iterations ratios: " ^ string_of_int it_ratios)
@@ -237,31 +242,32 @@
 
 in
 
-fun log_data id log (Data
-   (ShData{calls=sh_calls, lemmas=sh_lemmas,  max_lems=sh_max_lems, success=sh_success,
-      time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
-    MeData{calls=metis_calls0, proofs=metis_proofs0,
-      success=metis_success0, time=metis_time0, timeout=metis_timeout0,
-      lemmas=metis_lemmas0, posns=metis_posns0},
-    MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios},
-    MeData{calls=metis_calls, proofs=metis_proofs,
-      success=metis_success, time=metis_time, timeout=metis_timeout,
-      lemmas=metis_lemmas, posns=metis_posns})) =
-  if sh_calls > 0
-  then
-   (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
-    log_sh_data log sh_calls sh_success sh_lemmas sh_max_lems sh_time_isa sh_time_atp sh_time_atp_fail;
-    log "";
-    if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
-      metis_success metis_proofs metis_time metis_timeout metis_lemmas metis_posns else ();
-    log "";
-    if metis_calls0 > 0
-      then (log_min_data log min_succs ab_ratios it_ratios; log "";
-            log_metis_data log "unminimized " sh_calls sh_success metis_calls0
-              metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
-      else ()
-   )
-  else ()
+fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+  let
+    val ShData {calls=sh_calls, ...} = sh
+
+    fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else ()
+    fun log_me tag m =
+      log_me_data log tag sh_calls (tuple_of_me_data m)
+    fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
+      (log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2)))
+  in
+    if sh_calls > 0
+    then
+     (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
+      log_sh_data log (tuple_of_sh_data sh);
+      log "";
+      if not mini
+      then log_metis ("", me_u) ("fully-typed ", me_uft)
+      else
+        app_if me_u (fn () =>
+         (log_metis ("unminimized ", me_u) ("unminimized fully-typed ", me_uft);
+          log "";
+          app_if me_m (fn () =>
+            (log_min_data log (tuple_of_min_data min); log "";
+             log_metis ("", me_m) ("fully-typed ", me_mft))))))
+    else ()
+  end
 
 end
 
@@ -397,54 +403,63 @@
   end
 
 
-fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout,
-    inc_metis_lemmas, inc_metis_posns) args name named_thms id
+fun run_metis full m name named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
-    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
+    fun metis thms ctxt =
+      if full then MetisTools.metisFT_tac ctxt thms
+      else MetisTools.metis_tac ctxt thms
     fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
-      | with_time (true, t) = (change_data id inc_metis_success;
-          change_data id (inc_metis_lemmas (length named_thms));
-          change_data id (inc_metis_time t);
-          change_data id (inc_metis_posns pos);
-          if name = "proof" then change_data id inc_metis_proofs else ();
+      | with_time (true, t) = (change_data id (inc_metis_success m);
+          change_data id (inc_metis_lemmas m (length named_thms));
+          change_data id (inc_metis_time m t);
+          change_data id (inc_metis_posns m pos);
+          if name = "proof" then change_data id (inc_metis_proofs m) else ();
           "succeeded (" ^ string_of_int t ^ ")")
     fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
-      handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
+      handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m); "timeout")
            | ERROR msg => "error: " ^ msg
 
     val _ = log separator
-    val _ = change_data id inc_metis_calls
+    val _ = change_data id (inc_metis_calls m)
   in
     maps snd named_thms
     |> timed_metis
     |> log o prefix (metis_tag id) 
   end
 
-fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
+fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
   let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre))  (* FIXME ?? *) in
   if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
   then () else
   let
-    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time,
-        inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
-    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0,
-        inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
     val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
     val minimize = AList.defined (op =) args minimizeK
+    val metis_ft = AList.defined (op =) args metis_ftK
+
+    fun apply_metis m1 m2 =
+      if metis_ft
+      then
+        Mirabelle.app_timeout metis_tag
+          (run_metis false m1 name (these (!named_thms)))
+          (Mirabelle.catch metis_tag
+            (run_metis true m2 name (these (!named_thms)))) id st
+      else
+        Mirabelle.catch metis_tag
+          (run_metis false m1 name (these (!named_thms))) id st
   in 
+    change_data id (set_mini minimize);
     Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
     if is_some (!named_thms)
+    then
+     (apply_metis Unminimized UnminimizedFT;
+      if minimize andalso not (null (these (!named_thms)))
       then
-       (if minimize
-          then Mirabelle.catch metis_tag (run_metis metis0_fns args name (these (!named_thms))) id st
-          else ();
-       if minimize andalso not(null(these(!named_thms)))
-         then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
-         else ();
-       Mirabelle.catch metis_tag (run_metis metis_fns args name (these (!named_thms))) id st)
+       (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
+        apply_metis Minimized MinimizedFT)
+      else ())
     else ()
   end
   end

--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed Dec 09 11:53:51 2009 +0100
@@ -46,6 +46,8 @@
   echo "    * minimize_timeout=TIME: timeout for each minimization step (seconds of"
   echo "      process time)"
   echo "    * metis: apply metis to the theorems found by sledgehammer"
+  echo "    * metis_ft: apply metis with fully-typed encoding to the theorems found"
+  echo "      by sledgehammer"
   echo
   echo "  FILES is a list of theory files, where each file is either NAME.thy"
   echo "  or NAME.thy[START:END] and START and END are numbers indicating the"

--- a/src/HOL/SMT/Tools/smt_translate.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -284,7 +284,7 @@
     | mark f false t = f false t #>> app formula_marker o single
   fun mark' f false t = f true t #>> app term_marker o single
     | mark' f true t = f true t
-  val mark_term = app term_marker o single
+  fun mark_term (t : (sym, typ) sterm) = app term_marker [t]
   fun lift_term_marker c ts =
     let val rem = (fn SApp (SConst (@{const_name term}, _), [t]) => t | t => t)
     in mark_term (SApp (c, map rem ts)) end

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -2586,11 +2586,11 @@
     val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
     val eval =
       if random then
-        Code_ML.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
+        Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
             (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
           |> Random_Engine.run
       else
-        Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
+        Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
   in (T, eval) end;
 
 fun values ctxt param_user_modes options k t_compr =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -106,7 +106,7 @@
       mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
       (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
     val _ = tracing (Syntax.string_of_term ctxt' qc_term)
-    val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+    val compile = Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
       (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
       thy'' qc_term []
   in

--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -379,7 +379,7 @@
   let
     val Ts = (map snd o fst o strip_abs) t;
     val t' = mk_generator_expr thy t Ts;
-    val compile = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+    val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
       (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
   in compile #> Random_Engine.run end;
 
@@ -388,7 +388,7 @@
 
 val setup = Typecopy.interpretation ensure_random_typecopy
   #> Datatype.interpretation ensure_random_datatype
-  #> Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
+  #> Code_Target.extend_target (target, (Code_Eval.target, K I))
   #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
 
 end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_eval.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -0,0 +1,153 @@
+(*  Title:      Tools/code/code_eval.ML_
+    Author:     Florian Haftmann, TU Muenchen
+
+Runtime services building on code generation into implementation language SML.
+*)
+
+signature CODE_EVAL =
+sig
+  val target: string
+  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
+    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+  val evaluation_code: theory -> string list -> string list
+    -> string * ((string * string) list * (string * string) list)
+  val setup: theory -> theory
+end;
+
+structure Code_Eval : CODE_EVAL =
+struct
+
+(** generic **)
+
+val target = "Eval";
+
+val eval_struct_name = "Code";
+
+fun evaluation_code thy tycos consts =
+  let
+    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
+    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+    val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
+      eval_struct_name naming program (consts' @ tycos');
+    val (consts'', tycos'') = chop (length consts') target_names;
+    val consts_map = map2 (fn const => fn NONE =>
+        error ("Constant " ^ (quote o Code.string_of_const thy) const
+          ^ "\nhas a user-defined serialization")
+      | SOME const'' => (const, const'')) consts consts''
+    val tycos_map = map2 (fn tyco => fn NONE =>
+        error ("Type " ^ (quote o Sign.extern_type thy) tyco
+          ^ "\nhas a user-defined serialization")
+      | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+  in (ml_code, (tycos_map, consts_map)) end;
+
+
+(** evaluation **)
+
+fun eval some_target reff postproc thy t args =
+  let
+    val ctxt = ProofContext.init thy;
+    fun evaluator naming program ((_, (_, ty)), t) deps =
+      let
+        val _ = if Code_Thingol.contains_dictvar t then
+          error "Term to be evaluated contains free dictionaries" else ();
+        val value_name = "Value.VALUE.value"
+        val program' = program
+          |> Graph.new_node (value_name,
+              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
+          |> fold (curry Graph.add_edge value_name) deps;
+        val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
+          (the_default target some_target) "" naming program' [value_name];
+        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
+          ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
+      in ML_Context.evaluate ctxt false reff sml_code end;
+  in Code_Thingol.eval thy postproc evaluator t end;
+
+
+(** instrumentalization by antiquotation **)
+
+local
+
+structure CodeAntiqData = Proof_Data
+(
+  type T = (string list * string list) * (bool * (string
+    * (string * ((string * string) list * (string * string) list)) lazy));
+  fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
+);
+
+val is_first_occ = fst o snd o CodeAntiqData.get;
+
+fun register_code new_tycos new_consts ctxt =
+  let
+    val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
+    val tycos' = fold (insert (op =)) new_tycos tycos;
+    val consts' = fold (insert (op =)) new_consts consts;
+    val (struct_name', ctxt') = if struct_name = ""
+      then ML_Antiquote.variant eval_struct_name ctxt
+      else (struct_name, ctxt);
+    val acc_code = Lazy.lazy (fn () => evaluation_code (ProofContext.theory_of ctxt) tycos' consts');
+  in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
+
+fun register_const const = register_code [] [const];
+
+fun register_datatype tyco constrs = register_code [tyco] constrs;
+
+fun print_const const all_struct_name tycos_map consts_map =
+  (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
+
+fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
+  let
+    val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+    fun check_base name name'' =
+      if upperize (Long_Name.base_name name) = upperize name''
+      then () else error ("Name as printed " ^ quote name''
+        ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
+    val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
+    val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
+    val _ = check_base tyco tyco'';
+    val _ = map2 check_base constrs constrs'';
+  in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
+
+fun print_code struct_name is_first print_it ctxt =
+  let
+    val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
+    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
+    val ml_code = if is_first then ml_code
+      else "";
+    val all_struct_name = Long_Name.append struct_name struct_code_name;
+  in (ml_code, print_it all_struct_name tycos_map consts_map) end;
+
+in
+
+fun ml_code_antiq raw_const {struct_name, background} =
+  let
+    val const = Code.check_const (ProofContext.theory_of background) raw_const;
+    val is_first = is_first_occ background;
+    val background' = register_const const background;
+  in (print_code struct_name is_first (print_const const), background') end;
+
+fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
+  let
+    val thy = ProofContext.theory_of background;
+    val tyco = Sign.intern_type thy raw_tyco;
+    val constrs = map (Code.check_const thy) raw_constrs;
+    val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
+    val _ = if eq_set (op =) (constrs, constrs') then ()
+      else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
+    val is_first = is_first_occ background;
+    val background' = register_datatype tyco constrs background;
+  in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
+
+end; (*local*)
+
+
+(** Isar setup **)
+
+val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
+val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
+  (Args.tyname --| Scan.lift (Args.$$$ "=")
+    -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
+      >> ml_code_datatype_antiq);
+
+val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
+
+end; (*struct*)

--- a/src/Tools/Code/code_ml.ML	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/Tools/Code/code_ml.ML	Wed Dec 09 11:53:51 2009 +0100
@@ -6,9 +6,9 @@
 
 signature CODE_ML =
 sig
-  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
-    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
-  val target_Eval: string
+  val target_SML: string
+  val evaluation_code_of: theory -> string -> string
+    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   val setup: theory -> theory
 end;
 
@@ -26,7 +26,6 @@
 
 val target_SML = "SML";
 val target_OCaml = "OCaml";
-val target_Eval = "Eval";
 
 datatype ml_binding =
     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
@@ -340,7 +339,9 @@
           end;
   in print_stmt end;
 
-fun print_sml_module name some_decls body = Pretty.chunks2 (
+fun print_sml_module name some_decls body = if name = ""
+  then Pretty.chunks2 body
+  else Pretty.chunks2 (
     Pretty.chunks (
       str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
       :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -664,7 +665,9 @@
           end;
   in print_stmt end;
 
-fun print_ocaml_module name some_decls body = Pretty.chunks2 (
+fun print_ocaml_module name some_decls body = if name = ""
+  then Pretty.chunks2 body
+  else Pretty.chunks2 (
     Pretty.chunks (
       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
       :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -937,142 +940,15 @@
 end; (*local*)
 
 
-(** ML (system language) code for evaluation and instrumentalization **)
-
-val eval_struct_name = "Code"
-
-fun eval_code_of some_target with_struct thy =
-  let
-    val target = the_default target_Eval some_target;
-    val serialize = if with_struct then fn _ => fn [] =>
-        serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true
-      else fn _ => fn [] => 
-        serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true;
-  in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
-
-
-(* evaluation *)
-
-fun eval some_target reff postproc thy t args =
-  let
-    val ctxt = ProofContext.init thy;
-    fun evaluator naming program ((_, (_, ty)), t) deps =
-      let
-        val _ = if Code_Thingol.contains_dictvar t then
-          error "Term to be evaluated contains free dictionaries" else ();
-        val value_name = "Value.VALUE.value"
-        val program' = program
-          |> Graph.new_node (value_name,
-              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
-          |> fold (curry Graph.add_edge value_name) deps;
-        val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name];
-        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
-          ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
-      in ML_Context.evaluate ctxt false reff sml_code end;
-  in Code_Thingol.eval thy postproc evaluator t end;
-
-
-(* instrumentalization by antiquotation *)
-
-local
-
-structure CodeAntiqData = Proof_Data
-(
-  type T = (string list * string list) * (bool * (string
-    * (string * ((string * string) list * (string * string) list)) lazy));
-  fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
-);
-
-val is_first_occ = fst o snd o CodeAntiqData.get;
+(** for instrumentalization **)
 
-fun delayed_code thy tycos consts () =
-  let
-    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
-    val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
-    val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos');
-    val (consts'', tycos'') = chop (length consts') target_names;
-    val consts_map = map2 (fn const => fn NONE =>
-        error ("Constant " ^ (quote o Code.string_of_const thy) const
-          ^ "\nhas a user-defined serialization")
-      | SOME const'' => (const, const'')) consts consts''
-    val tycos_map = map2 (fn tyco => fn NONE =>
-        error ("Type " ^ (quote o Sign.extern_type thy) tyco
-          ^ "\nhas a user-defined serialization")
-      | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
-  in (ml_code, (tycos_map, consts_map)) end;
-
-fun register_code new_tycos new_consts ctxt =
-  let
-    val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
-    val tycos' = fold (insert (op =)) new_tycos tycos;
-    val consts' = fold (insert (op =)) new_consts consts;
-    val (struct_name', ctxt') = if struct_name = ""
-      then ML_Antiquote.variant eval_struct_name ctxt
-      else (struct_name, ctxt);
-    val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts');
-  in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
-
-fun register_const const = register_code [] [const];
-
-fun register_datatype tyco constrs = register_code [tyco] constrs;
-
-fun print_const const all_struct_name tycos_map consts_map =
-  (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
-
-fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
-  let
-    val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-    fun check_base name name'' =
-      if upperize (Long_Name.base_name name) = upperize name''
-      then () else error ("Name as printed " ^ quote name''
-        ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
-    val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
-    val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
-    val _ = check_base tyco tyco'';
-    val _ = map2 check_base constrs constrs'';
-  in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
-
-fun print_code struct_name is_first print_it ctxt =
-  let
-    val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
-    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
-    val ml_code = if is_first then ml_code
-      else "";
-    val all_struct_name = Long_Name.append struct_name struct_code_name;
-  in (ml_code, print_it all_struct_name tycos_map consts_map) end;
-
-in
-
-fun ml_code_antiq raw_const {struct_name, background} =
-  let
-    val const = Code.check_const (ProofContext.theory_of background) raw_const;
-    val is_first = is_first_occ background;
-    val background' = register_const const background;
-  in (print_code struct_name is_first (print_const const), background') end;
-
-fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
-  let
-    val thy = ProofContext.theory_of background;
-    val tyco = Sign.intern_type thy raw_tyco;
-    val constrs = map (Code.check_const thy) raw_constrs;
-    val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
-    val _ = if eq_set (op =) (constrs, constrs') then ()
-      else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
-    val is_first = is_first_occ background;
-    val background' = register_datatype tyco constrs background;
-  in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
-
-end; (*local*)
+fun evaluation_code_of thy target struct_name =
+  Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
+    serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
 
 
 (** Isar setup **)
 
-val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
-val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
-  (Args.tyname --| Scan.lift (Args.$$$ "=")
-    -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
-      >> ml_code_datatype_antiq);
-
 fun isar_seri_sml module_name =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   >> (fn with_signatures => serialize_ml target_SML
@@ -1087,7 +963,6 @@
 val setup =
   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
-  #> Code_Target.extend_target (target_Eval, (target_SML, K I))
   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         print_typ (INFX (1, X)) ty1,

--- a/src/Tools/Code_Generator.thy	Tue Dec 08 17:55:07 2009 +0100
+++ b/src/Tools/Code_Generator.thy	Wed Dec 09 11:53:51 2009 +0100
@@ -16,6 +16,7 @@
   "~~/src/Tools/Code/code_printer.ML"
   "~~/src/Tools/Code/code_target.ML"
   "~~/src/Tools/Code/code_ml.ML"
+  "~~/src/Tools/Code/code_eval.ML"
   "~~/src/Tools/Code/code_haskell.ML"
   "~~/src/Tools/nbe.ML"
 begin
@@ -23,6 +24,7 @@
 setup {*
   Code_Preproc.setup
   #> Code_ML.setup
+  #> Code_Eval.setup
   #> Code_Haskell.setup
   #> Nbe.setup
 *}