--- a/src/HOL/Tools/meson.ML Wed Jan 11 18:46:31 2006 +0100
+++ b/src/HOL/Tools/meson.ML Fri Jan 13 01:12:58 2006 +0100
@@ -443,7 +443,7 @@
(*Expand all definitions (presumably of Skolem functions) in a proof state.*)
fun expand_defs_tac st =
let val defs = filter (can dest_equals) (#hyps (crep_thm st))
- in ProofContext.export_def false defs st end;
+ in ProofContext.def_export false defs st end;
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*)
fun MESON cltac i st =