1.1 --- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Wed Jun 11 19:15:54 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Wed Jun 11 19:15:55 2014 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4      Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
     1.5      Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
     1.6      Modus_Ponens_Oeq | Th_Lemma of string
     1.7 +  val is_assumption: z3_rule -> bool
     1.8    val string_of_rule: z3_rule -> string
     1.9  
    1.10    (*proofs*)
    1.11 @@ -113,6 +114,13 @@
    1.12    ("sk", Skolemize),
    1.13    ("mp~", Modus_Ponens_Oeq)]
    1.14  
    1.15 +fun is_assumption Asserted = true
    1.16 +  | is_assumption Goal = true
    1.17 +  | is_assumption Hypothesis = true
    1.18 +  | is_assumption Intro_Def = true
    1.19 +  | is_assumption Skolemize = true
    1.20 +  | is_assumption _ = false
    1.21 +
    1.22  fun rule_of_string name =
    1.23    (case Symtab.lookup rule_names name of
    1.24      SOME rule => rule

     2.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Wed Jun 11 19:15:54 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Wed Jun 11 19:15:55 2014 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4  
     2.5  fun replay_thm ctxt assumed nthms
     2.6      (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
     2.7 -  if Z3_New_Replay_Methods.is_assumption rule then
     2.8 +  if Z3_New_Proof.is_assumption rule then
     2.9      (case Inttab.lookup assumed id of
    2.10        SOME (_, thm) => thm
    2.11      | NONE => Thm.assume (SMT2_Util.certify ctxt concl))
    2.12 @@ -115,7 +115,7 @@
    2.13  
    2.14      fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
    2.15          (cx as ((iidths, thms), (ctxt, ptab))) =
    2.16 -      if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
    2.17 +      if Z3_New_Proof.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
    2.18          let
    2.19            val ct = SMT2_Util.certify ctxt concl
    2.20            val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))

     3.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Wed Jun 11 19:15:54 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Wed Jun 11 19:15:55 2014 +0200
     3.3 @@ -49,7 +49,6 @@
     3.4    val nnf_neg: z3_method
     3.5    val mp_oeq: z3_method
     3.6    val th_lemma: string -> z3_method
     3.7 -  val is_assumption: Z3_New_Proof.z3_rule -> bool
     3.8    val method_for: Z3_New_Proof.z3_rule -> z3_method
     3.9  end
    3.10  
    3.11 @@ -646,13 +645,6 @@
    3.12  
    3.13  (* mapping of rules to methods *)
    3.14  
    3.15 -fun is_assumption Z3_New_Proof.Asserted = true
    3.16 -  | is_assumption Z3_New_Proof.Goal = true
    3.17 -  | is_assumption Z3_New_Proof.Hypothesis = true
    3.18 -  | is_assumption Z3_New_Proof.Intro_Def = true
    3.19 -  | is_assumption Z3_New_Proof.Skolemize = true
    3.20 -  | is_assumption _ = false
    3.21 -
    3.22  fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
    3.23  fun assumed rule ctxt = replay_error ctxt "Assumed" rule
    3.24