1.1 --- a/src/HOL/Tools/meson.ML	Wed Dec 06 17:08:19 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Dec 06 21:18:55 2006 +0100
     1.3 @@ -520,7 +520,7 @@
     1.4  (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
     1.5  fun expand_defs_tac st =
     1.6    let val defs = filter (can dest_equals) (#hyps (crep_thm st))
     1.7 -  in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
     1.8 +  in  PRIMITIVE (LocalDefs.expand defs) st  end;
     1.9  
    1.10  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
    1.11  fun MESON cltac i st =