# HG changeset patch
# User wenzelm
# Date 1138465731 -3600
# Node ID ad8bc3e55aa3d23f4af3f41fa7891b16b91aba68
# Parent  aebd7f315b924409b65dbfa12f01c7caa03f0d0e
LocalDefs.def_export;

diff -r aebd7f315b92 -r ad8bc3e55aa3 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sat Jan 28 17:28:50 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Jan 28 17:28:51 2006 +0100
@@ -441,7 +441,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.def_export false defs st  end;
+  in  LocalDefs.def_export false defs st  end;
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
 fun MESON cltac i st =