src/HOL/Tools/meson.ML
changeset 20288 8ff4a0ea49b2
parent 20134 73cb53843190
child 20361 1aaf9ebe248d
--- a/src/HOL/Tools/meson.ML	Wed Aug 02 22:26:39 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Aug 02 22:26:40 2006 +0200
@@ -451,7 +451,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  LocalDefs.def_export false defs st  end;
+  in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
 fun MESON cltac i st =