--- a/src/Provers/clasimp.ML Sun Aug 16 11:29:06 2015 +0200
+++ b/src/Provers/clasimp.ML Sun Aug 16 11:46:08 2015 +0200
@@ -90,7 +90,7 @@
Thm.declaration_attribute (fn th =>
Thm.attribute_declaration (add_iff
(Classical.safe_elim NONE, Classical.safe_intro NONE)
- (Classical.haz_elim NONE, Classical.haz_intro NONE)) th
+ (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th
#> Thm.attribute_declaration Simplifier.simp_add th);
val iff_add' =
@@ -122,7 +122,7 @@
fun slow_step_tac' ctxt =
Classical.appWrappers ctxt
- (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);
+ (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt);
in