diff -r b74143e10410 -r a92f96951355 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Jun 24 17:25:10 2005 +0200
@@ -29,13 +29,12 @@
   val depth_meson_tac	: int -> tactic
   val prolog_step_tac'	: thm list -> int -> tactic
   val iter_deepen_prolog_tac	: thm list -> tactic
-  val iter_deepen_meson_tac	: int -> tactic
+  val iter_deepen_meson_tac	: thm list -> int -> tactic
   val meson_tac		: int -> tactic
   val negate_head	: thm -> thm
   val select_literal	: int -> thm -> thm
   val skolemize_tac	: int -> tactic
   val make_clauses_tac	: int -> tactic
-  val meson_setup	: (theory -> theory) list
 end
 
 
@@ -61,6 +60,7 @@
 val disj_FalseD1 = thm "meson_disj_FalseD1";
 val disj_FalseD2 = thm "meson_disj_FalseD2";
 
+val depth_limit = ref 2000;
 
 (**** Operators for forward proof ****)
 
@@ -250,7 +250,8 @@
 fun make_horn crules th = make_horn crules (tryres(th,crules))
 			  handle THM _ => th;
 
-(*Generate Horn clauses for all contrapositives of a clause*)
+(*Generate Horn clauses for all contrapositives of a clause. The input, th,
+  is a HOL disjunction.*)
 fun add_contras crules (th,hcs) =
   let fun rots (0,th) = hcs
 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
@@ -267,7 +268,7 @@
 
     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
 
-(*Find an all-negative support clause*)
+(*Is the given disjunction an all-negative support clause?*)
 fun is_negative th = forall (not o #1) (literals (prop_of th));
 
 val neg_clauses = List.filter is_negative;
@@ -349,7 +350,7 @@
     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
 
 
-(*Convert a list of clauses to (contrapositive) Horn clauses*)
+(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =
     name_thms "Horn#"
       (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
@@ -366,7 +367,6 @@
 (*Return all negative clauses, as possible goal clauses*)
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
-
 fun skolemize_prems_tac prems =
     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
     REPEAT o (etac exE);
@@ -380,6 +380,7 @@
 
 (** Best-first search versions **)
 
+(*ths is a list of additional clauses (HOL disjunctions) to use.*)
 fun best_meson_tac sizef =
   MESON (fn cls =>
          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
@@ -398,7 +399,6 @@
                              depth_prolog_tac (make_horns cls)]);
 
 
-
 (** Iterative deepening version **)
 
 (*This version does only one inference per call;
@@ -415,16 +415,19 @@
 fun iter_deepen_prolog_tac horns =
     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
 
-val iter_deepen_meson_tac =
+fun iter_deepen_meson_tac ths =
   MESON (fn cls =>
-         (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
-                           (has_fewer_prems 1)
-                           (prolog_step_tac' (make_horns cls))));
+           case (gocls (cls@ths)) of
+           	[] => no_tac  (*no goal clauses*)
+              | goes => 
+		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
+				   (has_fewer_prems 1)
+				   (prolog_step_tac' (make_horns (cls@ths)))));
 
-fun meson_claset_tac cs =
-  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac);
+fun meson_claset_tac ths cs =
+  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
 
-val meson_tac = CLASET' meson_claset_tac;
+val meson_tac = CLASET' (meson_claset_tac []);
 
 
 (**** Code to support ordinary resolution, rather than Model Elimination ****)
@@ -496,28 +499,19 @@
                   (make_meta_clauses (make_clauses hyps))) 1)),
 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
      end);
-
-
-(*** proof method setup ***)
+     
+     
+(*** setup the special skoklemization methods ***)
 
-fun meson_meth ctxt =
-  Method.SIMPLE_METHOD' HEADGOAL
-    (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
+(*No CHANGED_PROP here, since these always appear in the preamble*)
 
-val skolemize_meth =
-  Method.SIMPLE_METHOD' HEADGOAL
-    (CHANGED_PROP o skolemize_tac);
+val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
+
+val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
 
-val make_clauses_meth =
-  Method.SIMPLE_METHOD' HEADGOAL
-    (CHANGED_PROP o make_clauses_tac);
-
-
-val meson_setup =
+val skolemize_setup =
  [Method.add_methods
-  [("meson", Method.ctxt_args meson_meth, 
-    "The MESON resolution proof procedure"),
-   ("skolemize", Method.no_args skolemize_meth, 
+  [("skolemize", Method.no_args skolemize_meth, 
     "Skolemization into existential quantifiers"),
    ("make_clauses", Method.no_args make_clauses_meth, 
     "Conversion to !!-quantified meta-level clauses")]];