# HG changeset patch
# User wenzelm
# Date 1137111178 -3600
# Node ID 598d3971eeb0124c180c9232601a2ae7d2df7558
# Parent  dde117622dace696123b023d1f06cf8d8ef9eb46
ProofContext.def_export;

diff -r dde117622dac -r 598d3971eeb0 src/HOL/Tools/meson.ML
--- 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 =