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;