src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15700 970e0293dfb3
parent 15643 5829f30fc20a
child 15736 1bb0399a9517
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 12 11:07:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 12 11:08:25 2005 +0200
     1.3 @@ -109,8 +109,8 @@
     1.4                                     (****************************************)
     1.5                                     (* add claset rules to array and write out as strings *)
     1.6                                     (****************************************)
     1.7 -                                   val claset_rules =claset_rules_of_thy Main.thy
     1.8 -                                   val claset = clausify_classical_rules_thy Main.thy
     1.9 +                                   val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
    1.10 +                                   val claset = ResAxioms.clausify_classical_rules_thy (the_context())
    1.11                                     val (claset_clauses,badthms) =  claset;
    1.12                                     val clausifiable_rules = remove_all badthms claset_rules;
    1.13                                     val named_claset = List.filter has_name clausifiable_rules;
    1.14 @@ -124,7 +124,7 @@
    1.15  
    1.16                                     val names_rules = zip good_names name_fol_cs;
    1.17                                     
    1.18 -                                   val new_clasrls = (fst(clausify_classical_rules name_fol_cs[]));
    1.19 +                                   val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[]));
    1.20  
    1.21                                     val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
    1.22  
    1.23 @@ -161,13 +161,13 @@
    1.24                                    (*********************)
    1.25                                    (* Get simpset rules *)
    1.26                                    (*********************)
    1.27 -                                  val (simpset_name_rules) =simpset_rules_of_thy Main.thy;
    1.28 +                                  val (simpset_name_rules) =simpset_rules_of_thy (the_context());
    1.29                                    val named_simps = List.filter has_name_pair simpset_name_rules;
    1.30  
    1.31                                    val simp_names = map fst named_simps;
    1.32                                    val simp_rules = map snd named_simps;
    1.33                                
    1.34 -                                  val (simpset_cls,badthms) = clausify_simpset_rules simp_rules [];
    1.35 +                                  val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
    1.36                                   (* 1137 clausif simps *)
    1.37                                    val clausifiable_simps = remove_all_simps badthms named_simps;
    1.38                                     
    1.39 @@ -179,7 +179,7 @@
    1.40                                      (* need to get names of claset_cluases so we can make sure we've*)
    1.41                                      (* got the same ones (ie. the named ones ) as the claset rules *)
    1.42                                      (* length 1374*)
    1.43 -                                    val new_simps = fst(clausify_simpset_rules simp_rules []);
    1.44 +                                    val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []);
    1.45                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    1.46  
    1.47                                      val stick_strs = map stick simpset_tptp_strs;