| changeset 32149 | ef59550a55d3 |
| parent 32010 | cb1a1c94b4cd |
| child 32155 | e2bf2f73b0c8 |
--- a/src/HOL/Tools/simpdata.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/simpdata.ML Thu Jul 23 18:44:09 2009 +0200 @@ -158,7 +158,7 @@ open Clasimp; val _ = ML_Antiquote.value "clasimpset" - (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"); + (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())"); val mksimps_pairs = [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),