diff -r f9cb300118ca -r c611b1412056 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Aug 25 18:46:24 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Aug 25 18:47:36 2006 +0200
@@ -15,6 +15,7 @@
 sig
   val size_of_subgoals	: thm -> int
   val make_cnf		: thm list -> thm -> thm list
+  val finish_cnf	: thm list -> thm list
   val make_nnf		: thm -> thm
   val make_nnf1		: thm -> thm
   val skolemize		: thm -> thm
@@ -36,7 +37,6 @@
   val select_literal	: int -> thm -> thm
   val skolemize_tac	: int -> tactic
   val make_clauses_tac	: int -> tactic
-  val check_is_fol_term : term -> term
 end
 
 
@@ -66,13 +66,29 @@
 
 (**** Operators for forward proof ****)
 
-(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
-fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
+
+(** First-order Resolution **)
+
+fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
+fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
+
+val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
+
+(*FIXME: currently does not "rename variables apart"*)
+fun first_order_resolve thA thB =
+  let val thy = theory_of_thm thA
+      val tmA = concl_of thA
+      fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
+      val Const("==>",_) $ tmB $ _ = prop_of thB
+      val (tyenv,tenv) = match tmB
+      val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
+  in  thA RS (cterm_instantiate ct_pairs thB)  end
+  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
 
 (*raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rls) = 
   let fun tryall [] = raise THM("tryres", 0, th::rls)
-        | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
+        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
   in  tryall rls  end;
   
 (*Permits forward proof from rules that discharge assumptions*)
@@ -189,6 +205,11 @@
 
 val has_meta_conn = 
     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
+
+fun apply_skolem_ths (th, rls) = 
+  let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
+        | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
+  in  tryall rls  end;
   
 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   Strips universal quantifiers and breaks up conjunctions.
@@ -200,13 +221,12 @@
 	then th::ths (*no work to do, terminate*)
 	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
 	    Const ("op &", _) => (*conjunction*)
-		cnf_aux (th RS conjunct1,
-			      cnf_aux (th RS conjunct2, ths))
+		cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
 	  | Const ("All", _) => (*universal quantifier*)
 	        cnf_aux (freeze_spec th,  ths)
 	  | Const ("Ex", _) => 
 	      (*existential quantifier: Insert Skolem functions*)
-	      cnf_aux (tryres (th,skoths), ths)
+	      cnf_aux (apply_skolem_ths (th,skoths), ths)
 	  | Const ("op |", _) => (*disjunction*)
 	      let val tac =
 		  (METAHYPS (resop cnf_nil) 1) THEN
@@ -224,9 +244,10 @@
   but don't discharge assumptions.*)
 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
 
-fun make_cnf skoths th = 
-  filter (not o is_taut) 
-    (map (refl_clause o generalize) (cnf skoths (th, [])));
+fun make_cnf skoths th = cnf skoths (th, []);
+
+(*Generalization, removal of redundant equalities, removal of tautologies.*)
+fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
 
 
 (**** Removal of duplicate literals ****)
@@ -303,13 +324,6 @@
 	 has_bool_arg_const t  orelse  
 	 has_meta_conn t);
 
-(*FIXME: replace this by the boolean-valued version above!*)
-fun check_is_fol_term t =
-    if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
-
-fun check_is_fol th = (check_is_fol_term (prop_of th); th);
-
-
 (*Create a meta-level Horn clause*)
 fun make_horn crules th = make_horn crules (tryres(th,crules))
 			  handle THM _ => th;
@@ -426,7 +440,6 @@
 fun make_clauses ths =
     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
 
-
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =
     name_thms "Horn#"
@@ -461,7 +474,7 @@
 		      EVERY1 [skolemize_prems_tac negs,
 			      METAHYPS (cltac o make_clauses)]) 1,
             expand_defs_tac]) i st
-  handle TERM _ => no_tac st;	(*probably from check_is_fol*)		      
+  handle THM _ => no_tac st;	(*probably from make_meta_clause, not first-order*)		      
 
 (** Best-first search versions **)
 
@@ -531,7 +544,9 @@
 
 (*Converting one clause*)
 fun make_meta_clause th = 
-    negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
+  if is_fol_term (prop_of th) 
+  then negated_asm_of_head (make_horn resolution_clause_rules th)
+  else raise THM("make_meta_clause", 0, [th]);
 
 fun make_meta_clauses ths =
     name_thms "MClause#"