# HG changeset patch
# User paulson
# Date 1141746633 -3600
# Node ID 27b91724809fc1520ca7f6441e43a4abfc112df4
# Parent  3e8006cbc925abb076cd4755f5a7e6a36d42173f
Indentation

diff -r 3e8006cbc925 -r 27b91724809f src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Mar 07 16:49:48 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Mar 07 16:50:33 2006 +0100
@@ -227,8 +227,7 @@
   | hashw_term ((Var(_,_)), w) = w
   | hashw_term ((Bound _), w) = w
   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
-  | hashw_term ((P$Q), w) =
-    hashw_term (Q, (hashw_term (P, w)));
+  | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
 
 fun hashw_pred (P,w) = 
     let val (p,args) = strip_comb P
@@ -241,8 +240,7 @@
 
 
 fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
-  | get_literals (Const("op |",_)$P$Q) lits =
-    get_literals Q (get_literals P lits)
+  | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   | get_literals lit lits = (lit::lits);
 
 
@@ -263,14 +261,14 @@
 
 fun insert_tms [] tms_names = tms_names
   | insert_tms ((tm,name)::tms_names) tms_names' =
-    if mem_tm tm tms_names' then insert_tms tms_names tms_names' else insert_tms tms_names ((tm,name)::tms_names');
+      if mem_tm tm tms_names' then insert_tms tms_names tms_names' 
+      else insert_tms tms_names ((tm,name)::tms_names');
 
 fun warning_thms [] = ()
   | warning_thms ((name,thm)::nthms) = 
-    let val nthm = name ^ ": " ^ (string_of_thm thm)
-    in
-	(warning nthm; warning_thms nthms)
-    end;
+      let val nthm = name ^ ": " ^ (string_of_thm thm)
+      in warning nthm; warning_thms nthms  end;
+ 
 (*Write out the claset, simpset and atpset rules of the supplied theory.*)
 (* also write supplied user rules, they are not relevance filtered *)
 fun get_clasimp_atp_lemmas ctxt goals user_thms (use_claset, use_simpset', use_atpset) run_filter =
@@ -290,17 +288,21 @@
       val user_rules = map put_name_pair user_thms
       val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms))
       fun ok (a,_) = not (banned a) 	   
-      val claset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms)
-			   else ResAxioms.clausify_rules_pairs_abs claset_thms
-      val simpset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok simpset_thms)
-			    else ResAxioms.clausify_rules_pairs_abs simpset_thms
-      val atpset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok atpset_thms)
-			   else ResAxioms.clausify_rules_pairs_abs atpset_thms
+      val claset_cls_tms = 
+            if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms)
+            else ResAxioms.clausify_rules_pairs_abs claset_thms
+      val simpset_cls_tms = 
+      	    if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok simpset_thms)
+	    else ResAxioms.clausify_rules_pairs_abs simpset_thms
+      val atpset_cls_tms = 
+      	    if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok atpset_thms)
+	    else ResAxioms.clausify_rules_pairs_abs atpset_thms
       val user_cls_tms = ResAxioms.clausify_rules_pairs_abs user_rules (* no filter here, because user supplied rules *)
       val cls_tms_list = make_unique (mk_clause_table 2200) 
-                                      (List.concat (user_cls_tms@atpset_cls_tms@simpset_cls_tms@claset_cls_tms))
+                           (List.concat (user_cls_tms@atpset_cls_tms@simpset_cls_tms@claset_cls_tms))
       val relevant_cls_tms_list =
-	  if run_filter then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_tms_list goals
+	  if run_filter 
+	  then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_tms_list goals
 	  else cls_tms_list
       val all_relevant_cls_tms_list = insert_tms (List.concat user_cls_tms) relevant_cls_tms_list (*ensure all user supplied rules are output*)	  
     in