src/Tools/intuitionistic.ML
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 55627 95c8ef02f04b
--- a/src/Tools/intuitionistic.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/Tools/intuitionistic.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -89,7 +89,7 @@
   Method.setup name
     (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
       (fn opt_lim => fn ctxt =>
-        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
+        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
     "intuitionistic proof search";
 
 end;