# HG changeset patch
# User blanchet
# Date 1402506955 -7200
# Node ID 853557cf2efa06c5634e4c8336f88fdcb7c5485b
# Parent  34018603e0d09c5d7c13da7bb6886f7291a7df44
tuned code

diff -r 34018603e0d0 -r 853557cf2efa src/HOL/Tools/SMT2/z3_new_proof.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Wed Jun 11 19:15:55 2014 +0200
@@ -15,6 +15,7 @@
     Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
     Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
     Modus_Ponens_Oeq | Th_Lemma of string
+  val is_assumption: z3_rule -> bool
   val string_of_rule: z3_rule -> string
 
   (*proofs*)
@@ -113,6 +114,13 @@
   ("sk", Skolemize),
   ("mp~", Modus_Ponens_Oeq)]
 
+fun is_assumption Asserted = true
+  | is_assumption Goal = true
+  | is_assumption Hypothesis = true
+  | is_assumption Intro_Def = true
+  | is_assumption Skolemize = true
+  | is_assumption _ = false
+
 fun rule_of_string name =
   (case Symtab.lookup rule_names name of
     SOME rule => rule
diff -r 34018603e0d0 -r 853557cf2efa src/HOL/Tools/SMT2/z3_new_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Wed Jun 11 19:15:55 2014 +0200
@@ -58,7 +58,7 @@
 
 fun replay_thm ctxt assumed nthms
     (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
-  if Z3_New_Replay_Methods.is_assumption rule then
+  if Z3_New_Proof.is_assumption rule then
     (case Inttab.lookup assumed id of
       SOME (_, thm) => thm
     | NONE => Thm.assume (SMT2_Util.certify ctxt concl))
@@ -115,7 +115,7 @@
 
     fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
         (cx as ((iidths, thms), (ctxt, ptab))) =
-      if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
+      if Z3_New_Proof.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
         let
           val ct = SMT2_Util.certify ctxt concl
           val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
diff -r 34018603e0d0 -r 853557cf2efa src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Wed Jun 11 19:15:54 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Wed Jun 11 19:15:55 2014 +0200
@@ -49,7 +49,6 @@
   val nnf_neg: z3_method
   val mp_oeq: z3_method
   val th_lemma: string -> z3_method
-  val is_assumption: Z3_New_Proof.z3_rule -> bool
   val method_for: Z3_New_Proof.z3_rule -> z3_method
 end
 
@@ -646,13 +645,6 @@
 
 (* mapping of rules to methods *)
 
-fun is_assumption Z3_New_Proof.Asserted = true
-  | is_assumption Z3_New_Proof.Goal = true
-  | is_assumption Z3_New_Proof.Hypothesis = true
-  | is_assumption Z3_New_Proof.Intro_Def = true
-  | is_assumption Z3_New_Proof.Skolemize = true
-  | is_assumption _ = false
-
 fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
 fun assumed rule ctxt = replay_error ctxt "Assumed" rule