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