src/HOL/Tools/SMT/z3_proof_reconstruction.ML
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 54883 dd04a8b654fc
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -38,16 +38,19 @@
     1.4      val merge = Net.merge eq
     1.5    )
     1.6  
     1.7 -  val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
     1.8 +  fun prep context =
     1.9 +    `Thm.prop_of o rewrite_rule (Context.proof_of context) [Z3_Proof_Literals.rewrite_true]
    1.10  
    1.11 -  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
    1.12 -  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
    1.13 +  fun ins thm context =
    1.14 +    context |> Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
    1.15 +  fun rem thm context =
    1.16 +    context |> Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
    1.17  
    1.18 -  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
    1.19 -  val del = Thm.declaration_attribute (Z3_Rules.map o del)
    1.20 +  val add = Thm.declaration_attribute ins
    1.21 +  val del = Thm.declaration_attribute rem
    1.22  in
    1.23  
    1.24 -val add_z3_rule = Z3_Rules.map o ins
    1.25 +val add_z3_rule = ins
    1.26  
    1.27  fun by_schematic_rule ctxt ct =
    1.28    the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)