src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15736 1bb0399a9517
parent 15700 970e0293dfb3
child 15774 9df37a0e935d
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Apr 15 12:00:00 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Apr 15 13:35:53 2005 +0200
     1.3 @@ -62,20 +62,6 @@
     1.4                  |SOME cls  => cls ;
     1.5        	        	
     1.6  
     1.7 -fun retr_thms ([]:MetaSimplifier.rrule list) = []
     1.8 -	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
     1.9 -
    1.10 -fun snds [] = []
    1.11 -   | snds ((x,y)::l) = y::(snds l);
    1.12 -
    1.13 -fun simpset_rules_of_thy thy =
    1.14 -     let val simpset = simpset_of thy
    1.15 -	val rules = #rules(fst (rep_ss simpset))
    1.16 -	val thms = retr_thms (snds(Net.dest rules))
    1.17 -     in	thms  end;
    1.18 -
    1.19 -
    1.20 -
    1.21  
    1.22  
    1.23  fun not_second c (a,b)  = not_equal b c;
    1.24 @@ -124,7 +110,7 @@
    1.25  
    1.26                                     val names_rules = zip good_names name_fol_cs;
    1.27                                     
    1.28 -                                   val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[]));
    1.29 +                                   val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
    1.30  
    1.31                                     val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
    1.32  
    1.33 @@ -161,25 +147,25 @@
    1.34                                    (*********************)
    1.35                                    (* Get simpset rules *)
    1.36                                    (*********************)
    1.37 -                                  val (simpset_name_rules) =simpset_rules_of_thy (the_context());
    1.38 +                                  val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
    1.39                                    val named_simps = List.filter has_name_pair simpset_name_rules;
    1.40  
    1.41 -                                  val simp_names = map fst named_simps;
    1.42 -                                  val simp_rules = map snd named_simps;
    1.43 +                                  val simp_names = map #1 named_simps;
    1.44 +                                  val simp_rules = map #2 named_simps;
    1.45                                
    1.46                                    val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
    1.47                                   (* 1137 clausif simps *)
    1.48                                    val clausifiable_simps = remove_all_simps badthms named_simps;
    1.49                                     
    1.50                                      val name_fol_simps = List.filter thm_is_fol clausifiable_simps ;
    1.51 -                                    val simp_names = map fst name_fol_simps;
    1.52 -                                    val simp_rules = map snd name_fol_simps;
    1.53 +                                    val simp_names = map #1 name_fol_simps;
    1.54 +                                    val simp_rules = map #2 name_fol_simps;
    1.55                                      
    1.56                                       (* 995 of these *)
    1.57                                      (* need to get names of claset_cluases so we can make sure we've*)
    1.58                                      (* got the same ones (ie. the named ones ) as the claset rules *)
    1.59                                      (* length 1374*)
    1.60 -                                    val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []);
    1.61 +                                    val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []);
    1.62                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    1.63  
    1.64                                      val stick_strs = map stick simpset_tptp_strs;