# HG changeset patch
# User paulson
# Date 1135355686 -3600
# Node ID c5861e128a95866a24f64fde19c1f991066fbeb5
# Parent  9b8b33098ced3bf7aacf20554a86ec00598dbde3
tidied

diff -r 9b8b33098ced -r c5861e128a95 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Dec 23 15:21:05 2005 +0100
+++ b/src/HOL/Tools/meson.ML	Fri Dec 23 17:34:46 2005 +0100
@@ -292,15 +292,6 @@
 (*Raises an exception if any Vars in the theorem mention type bool; they
   could cause make_horn to loop! Also rejects functions whose arguments are 
   Booleans or other functions.*)
-fun check_is_fol th = 
-  let val {prop,...} = rep_thm th
-  in if exists (has_bool o fastype_of) (term_vars prop)  orelse
-        not (Term.is_first_order ["all","All","Ex"] prop) orelse
-        has_bool_arg_const prop  orelse  
-        has_meta_conn prop
-  then raise THM ("check_is_fol", 0, [th]) else th
-  end;
-
 fun check_is_fol_term term =
     if exists (has_bool o fastype_of) (term_vars term)  orelse
         not (Term.is_first_order ["all","All","Ex"] term) orelse
@@ -308,6 +299,8 @@
         has_meta_conn term
     then raise TERM("check_is_fol_term",[term]) else term;
 
+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))
@@ -356,10 +349,12 @@
 		  handle INSERT => true;
 
 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
-fun TRYALL_eq_assume_tac 0 st = Seq.single st
-  | TRYALL_eq_assume_tac i st =
-       TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
-       handle THM _ => TRYALL_eq_assume_tac (i-1) st;
+fun TRYING_eq_assume_tac 0 st = Seq.single st
+  | TRYING_eq_assume_tac i st =
+       TRYING_eq_assume_tac (i-1) (eq_assumption i st)
+       handle THM _ => TRYING_eq_assume_tac (i-1) st;
+
+fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
 
 (*Loop checking: FAIL if trying to prove the same thing twice
   -- if *ANY* subgoal has repeated literals*)
@@ -371,7 +366,7 @@
 (* net_resolve_tac actually made it slower... *)
 fun prolog_step_tac horns i =
     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
-    TRYALL eq_assume_tac;
+    TRYALL_eq_assume_tac;
 
 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
@@ -458,7 +453,7 @@
 		      EVERY1 [skolemize_prems_tac negs,
 			      METAHYPS (cltac o make_clauses)]) 1,
             expand_defs_tac]) i st
-  handle THM _ => no_tac st;	(*probably from check_is_fol*)		      
+  handle TERM _ => no_tac st;	(*probably from check_is_fol*)		      
 
 (** Best-first search versions **)
 
@@ -549,6 +544,7 @@
 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
 fun select_literal i cl = negate_head (make_last i cl);
 
+
 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   expressed as a tactic (or Isar method).  Each assumption of the selected 
   goal is converted to NNF and then its existential quantifiers are pulled
@@ -556,8 +552,6 @@
   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   might generate many subgoals.*)
 
-
-
 val skolemize_tac = 
   SUBGOAL
     (fn (prop,_) =>
@@ -570,7 +564,6 @@
      end);
 
 
-
 (*Top-level conversion to meta-level clauses. Each clause has  
   leading !!-bound universal variables, to express generality. To get 
   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
diff -r 9b8b33098ced -r c5861e128a95 src/HOL/Tools/polyhash.ML
--- a/src/HOL/Tools/polyhash.ML	Fri Dec 23 15:21:05 2005 +0100
+++ b/src/HOL/Tools/polyhash.ML	Fri Dec 23 17:34:46 2005 +0100
@@ -4,7 +4,7 @@
  * See file mosml/copyrght/copyrght.att for details.
  *
  * Original author: John Reppy, AT&T Bell Laboratories, Murray Hill, NJ 07974
- * Current version largely by Joseph Hurd
+ * Current version from the Moscow ML distribution, copied by permission.
  *)
 
 (* Polyhash -- polymorphic hashtables as in the SML/NJ Library *)
@@ -382,26 +382,13 @@
 	  end
 
    (*Added by lcp.
-      This is essentially the hashpjw function described in Compilers:
+      This is essentially the  described in Compilers:
       Principles, Techniques, and Tools, by Aho, Sethi and Ullman.*)
- (*  local infix << >>
-	 val left = Word.fromInt (Word.wordSize - 4)
-	 val right = Word.fromInt (Word.wordSize - 8)
-	 open Word
-   in  
-   val mask = 0wxf << left
-   fun hashw (u,w) =
-     let val w' = (w << 0w4) + u
-	 val g = Word.andb(w', mask)  
-     in  
-	 if g <> 0w0 then Word.xorb(g, Word.xorb(w', g >> right))
-	 else w'
-     end;
-   end;*)
 
-   (*This version is also recommended by Aho et al. and does not trigger the Poly/ML bug*)
-   val hmulti = Word.fromInt 65599;
-   fun hashw (u,w) = Word.+ (u, Word.*(hmulti,w))
+   (*This hash function is recommended in Compilers: Principles, Techniques, and
+     Tools, by Aho, Sethi and Ullman. The hashpjw function, which they particularly
+     recommend, triggers a bug in versions of Poly/ML up to 4.2.0.*)
+   fun hashw (u,w) = Word.+ (u, Word.*(0w65599,w))
 
    fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w);
    
diff -r 9b8b33098ced -r c5861e128a95 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Fri Dec 23 15:21:05 2005 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Fri Dec 23 17:34:46 2005 +0100
@@ -284,9 +284,8 @@
 
 fun cnf_hyps_thms ctxt = 
     let val ths = ProofContext.prems_of ctxt
-	val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux ths)
     in
-	prems
+	ResClause.union_all (map ResAxioms.skolem_thm ths)
     end;
 
 (**** clausification ****)