src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
 changeset 58059 4e477dcd050a parent 58058 1a0b18176548 child 58957 c9e744ea8a38
```--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Thu Aug 28 00:40:38 2014 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -52,8 +52,8 @@
the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct)

val _ = Theory.setup
-  Global_Theory.add_thms_dynamic (@{binding z3_rule}, Net.content o Old_Z3_Rules.get))
+  Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get))

end

@@ -80,7 +80,7 @@
Pretty.big_list ("Z3 found a proof," ^
" but proof reconstruction failed at the following subgoal:")
(pretty_goal ctxt thms (Thm.term_of ct)),
-      Pretty.str ("Declaring a rule as [z3_rule] might solve this problem.")])
+      Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")])

fun apply [] ct = error (try_apply_err ct)
| apply (prover :: provers) ct =
@@ -870,7 +870,7 @@
Old_Z3_Proof_Parser.parse ctxt typs terms output

val simpset =
-      Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems z3_simp})
+      Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp})

val ((is, rules), cxp as (ctxt2, _)) =
add_asserted outer_ctxt rewrite_rules assms asserted ctxt1```