--- a/src/Provers/clasimp.ML Fri Oct 02 22:02:54 2009 +0200
+++ b/src/Provers/clasimp.ML Fri Oct 02 22:15:08 2009 +0200
@@ -141,7 +141,6 @@
val addXIs = modifier (ContextRules.intro_query NONE);
val addXEs = modifier (ContextRules.elim_query NONE);
-val addXDs = modifier (ContextRules.dest_query NONE);
val delXs = modifier ContextRules.rule_del;
in
@@ -266,9 +265,6 @@
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
-fun clasimp_method tac =
- Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
-
fun clasimp_method' tac =
Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);