1.1 --- a/src/HOL/Tools/meson.ML Wed Aug 02 22:26:39 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Wed Aug 02 22:26:40 2006 +0200
1.3 @@ -451,7 +451,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 LocalDefs.def_export false defs st end;
1.8 + in PRIMITIVE (LocalDefs.def_export false 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 =