changeset 35625 | 9c818cab0dd0 |
parent 33554 | 4601372337e4 |
child 36960 | 01594f816e3a |
--- a/src/Tools/intuitionistic.ML Sun Mar 07 11:57:16 2010 +0100 +++ b/src/Tools/intuitionistic.ML Sun Mar 07 12:19:47 2010 +0100 @@ -89,7 +89,7 @@ Method.setup name (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >> (fn opt_lim => fn ctxt => - SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim))) + SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim))) "intuitionistic proof search"; end;