# HG changeset patch
# User wenzelm
# Date 1165436335 -3600
# Node ID fcfc4afde6b9aee63a9f56765a397720914a04cf
# Parent  8ce2e9ef0bd2d6470d1fcccd0856755093c6bc2a
LocalDefs.expand;

diff -r 8ce2e9ef0bd2 -r fcfc4afde6b9 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Dec 06 17:08:19 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Wed Dec 06 21:18:55 2006 +0100
@@ -520,7 +520,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  PRIMITIVE (LocalDefs.def_export false defs) st  end;
+  in  PRIMITIVE (LocalDefs.expand defs) st  end;
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
 fun MESON cltac i st =