# HG changeset patch
# User paulson
# Date 1161595105 -7200
# Node ID 8f3dffd52db227b9b328418d8e2150ea9fa09ccf
# Parent  2c9f73fa973c3552cc38633b80bb5bfe92797082
meson method MUST NOT use all safe rules, only basic ones for the logical connectives.

diff -r 2c9f73fa973c -r 8f3dffd52db2 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Oct 23 11:17:29 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Oct 23 11:18:25 2006 +0200
@@ -688,7 +688,7 @@
 
 fun meson_meth ths ctxt =
   Method.SIMPLE_METHOD' HEADGOAL
-    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
+    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs);
 
 val meson_method_setup =
   Method.add_methods