src/Provers/clasimp.ML
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 58008 aa72531f972f
--- a/src/Provers/clasimp.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/Provers/clasimp.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -150,7 +150,7 @@
     TRY (Classical.safe_tac ctxt) THEN
     REPEAT_DETERM (FIRSTGOAL main_tac) THEN
     TRY (Classical.safe_tac (addSss ctxt)) THEN
-    prune_params_tac
+    prune_params_tac ctxt
   end;
 
 fun auto_tac ctxt = mk_auto_tac ctxt 4 2;