removed global ref dfg_format
authorimmler@in.tum.de
Thu Feb 26 10:13:43 2009 +0100 (2009-02-26)
changeset 30151629f3a92863e
parent 30150 4d5a98cebb24
child 30152 0ddd8028f98c
removed global ref dfg_format
src/HOL/Tools/atp_wrapper.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/atp_wrapper.ML	Wed Feb 25 10:02:10 2009 +0100
     1.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Thu Feb 26 10:13:43 2009 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  
     1.5  fun tptp_prover_opts_full max_new theory_const full command =
     1.6    external_prover
     1.7 -    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
     1.8 +    (ResAtp.write_problem_files false max_new theory_const)
     1.9      command
    1.10      ResReconstruct.find_failure_e_vamp_spass
    1.11      (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
    1.12 @@ -153,7 +153,7 @@
    1.13  (* SPASS *)
    1.14  
    1.15  fun spass_opts max_new theory_const = external_prover
    1.16 -  (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
    1.17 +  (ResAtp.write_problem_files true max_new theory_const)
    1.18    (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
    1.19    ResReconstruct.find_failure_e_vamp_spass
    1.20    ResReconstruct.lemma_list_dfg;
     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Feb 25 10:02:10 2009 +0100
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Feb 26 10:13:43 2009 +0100
     2.3 @@ -6,10 +6,7 @@
     2.4    val tvar_classes_of_terms : term list -> string list
     2.5    val tfree_classes_of_terms : term list -> string list
     2.6    val type_consts_of_terms : theory -> term list -> string list
     2.7 -  val write_problem_files : (theory -> bool -> Thm.thm list -> string ->
     2.8 -  (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list * ResClause.classrelClause list *
     2.9 -    ResClause.arityClause list -> string list -> ResHolClause.axiom_name list)
    2.10 -    -> int -> bool
    2.11 +  val write_problem_files : bool -> int -> bool
    2.12      -> (int -> Path.T) -> Proof.context * thm list * thm
    2.13      -> string list * ResHolClause.axiom_name Vector.vector list
    2.14  end;
    2.15 @@ -524,11 +521,10 @@
    2.16  (* TODO: problem file for *one* subgoal would be sufficient *)
    2.17  (*Write out problem files for each subgoal.
    2.18    Argument probfile generates filenames from subgoal-number
    2.19 -  Argument writer is either a tptp_write_file or dfg_write_file from ResHolClause
    2.20    Arguments max_new and theory_const are booleans controlling relevance_filter
    2.21      (necessary for different provers)
    2.22 -  *)
    2.23 -fun write_problem_files writer max_new theory_const probfile (ctxt, chain_ths, th) =
    2.24 +*)
    2.25 +fun write_problem_files dfg max_new theory_const probfile (ctxt, chain_ths, th) =
    2.26    let val goals = Thm.prems_of th
    2.27        val thy = ProofContext.theory_of ctxt
    2.28        fun get_neg_subgoals [] _ = []
    2.29 @@ -548,6 +544,7 @@
    2.30        val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
    2.31        (*clauses relevant to goal gl*)
    2.32        val axcls_list = map (fn ngcls => white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of ngcls)) goal_cls
    2.33 +      val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
    2.34        fun write_all [] [] _ = []
    2.35          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
    2.36              let val fname = File.platform_path (probfile k)
    2.37 @@ -561,7 +558,7 @@
    2.38                  and supers = tvar_classes_of_terms axtms
    2.39                  and tycons = type_consts_of_terms thy (ccltms@axtms)
    2.40                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
    2.41 -                val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
    2.42 +                val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
    2.43                  val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
    2.44                  val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
    2.45                  val thm_names = Vector.fromList clnames
     3.1 --- a/src/HOL/Tools/res_clause.ML	Wed Feb 25 10:02:10 2009 +0100
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Feb 26 10:13:43 2009 +0100
     3.3 @@ -27,9 +27,8 @@
     3.4    val make_fixed_var : string -> string
     3.5    val make_schematic_type_var : string * int -> string
     3.6    val make_fixed_type_var : string -> string
     3.7 -  val dfg_format: bool ref
     3.8 -  val make_fixed_const : string -> string
     3.9 -  val make_fixed_type_const : string -> string
    3.10 +  val make_fixed_const : bool -> string -> string
    3.11 +  val make_fixed_type_const : bool -> string -> string
    3.12    val make_type_class : string -> string
    3.13    datatype kind = Axiom | Conjecture
    3.14    type axiom_name = string
    3.15 @@ -50,6 +49,7 @@
    3.16    datatype classrelClause = ClassrelClause of
    3.17     {axiom_name: axiom_name, subclass: class, superclass: class}
    3.18    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
    3.19 +  val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list
    3.20    val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
    3.21    val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
    3.22    val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
    3.23 @@ -197,28 +197,26 @@
    3.24  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    3.25  
    3.26  (*HACK because SPASS truncates identifiers to 63 characters :-(( *)
    3.27 -val dfg_format = ref false;
    3.28 -
    3.29  (*32-bit hash,so we expect no collisions unless there are around 65536 long identifiers...*)
    3.30 -fun controlled_length s =
    3.31 -  if size s > 60 andalso !dfg_format
    3.32 +fun controlled_length dfg_format s =
    3.33 +  if size s > 60 andalso dfg_format
    3.34    then Word.toString (Polyhash.hashw_string(s,0w0))
    3.35    else s;
    3.36  
    3.37 -fun lookup_const c =
    3.38 +fun lookup_const dfg c =
    3.39      case Symtab.lookup const_trans_table c of
    3.40          SOME c' => c'
    3.41 -      | NONE => controlled_length (ascii_of c);
    3.42 +      | NONE => controlled_length dfg (ascii_of c);
    3.43  
    3.44 -fun lookup_type_const c =
    3.45 +fun lookup_type_const dfg c =
    3.46      case Symtab.lookup type_const_trans_table c of
    3.47          SOME c' => c'
    3.48 -      | NONE => controlled_length (ascii_of c);
    3.49 +      | NONE => controlled_length dfg (ascii_of c);
    3.50  
    3.51 -fun make_fixed_const "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
    3.52 -  | make_fixed_const c      = const_prefix ^ lookup_const c;
    3.53 +fun make_fixed_const _ "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
    3.54 +  | make_fixed_const dfg c      = const_prefix ^ lookup_const dfg c;
    3.55  
    3.56 -fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c;
    3.57 +fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
    3.58  
    3.59  fun make_type_class clas = class_prefix ^ ascii_of clas;
    3.60  
    3.61 @@ -251,13 +249,13 @@
    3.62  
    3.63  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
    3.64    TVars it contains.*)
    3.65 -fun type_of (Type (a, Ts)) =
    3.66 -      let val (folTyps, ts) = types_of Ts
    3.67 -          val t = make_fixed_type_const a
    3.68 +fun type_of dfg (Type (a, Ts)) =
    3.69 +      let val (folTyps, ts) = types_of dfg Ts
    3.70 +          val t = make_fixed_type_const dfg a
    3.71        in (Comp(t,folTyps), ts) end
    3.72 -  | type_of T = (atomic_type T, [T])
    3.73 -and types_of Ts =
    3.74 -      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    3.75 +  | type_of dfg T = (atomic_type T, [T])
    3.76 +and types_of dfg Ts =
    3.77 +      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    3.78        in (folTyps, union_all ts) end;
    3.79  
    3.80  (*Make literals for sorted type variables*)
    3.81 @@ -317,12 +315,12 @@
    3.82    | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
    3.83  
    3.84  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
    3.85 -fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
    3.86 +fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) =
    3.87     let val tvars = gen_TVars (length args)
    3.88         val tvars_srts = ListPair.zip (tvars,args)
    3.89     in
    3.90        ArityClause {axiom_name = axiom_name, 
    3.91 -                   conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
    3.92 +                   conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars),
    3.93                     premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
    3.94     end;
    3.95  
    3.96 @@ -354,20 +352,20 @@
    3.97  
    3.98  (** Isabelle arities **)
    3.99  
   3.100 -fun arity_clause _ _ (tcons, []) = []
   3.101 -  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   3.102 -      arity_clause seen n (tcons,ars)
   3.103 -  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   3.104 +fun arity_clause dfg _ _ (tcons, []) = []
   3.105 +  | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   3.106 +      arity_clause dfg seen n (tcons,ars)
   3.107 +  | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
   3.108        if class mem_string seen then (*multiple arities for the same tycon, class pair*)
   3.109 -          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   3.110 -          arity_clause seen (n+1) (tcons,ars)
   3.111 +          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   3.112 +          arity_clause dfg seen (n+1) (tcons,ars)
   3.113        else
   3.114 -          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
   3.115 -          arity_clause (class::seen) n (tcons,ars)
   3.116 +          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) ::
   3.117 +          arity_clause dfg (class::seen) n (tcons,ars)
   3.118  
   3.119 -fun multi_arity_clause [] = []
   3.120 -  | multi_arity_clause ((tcons,ars) :: tc_arlists) =
   3.121 -      arity_clause [] 1 (tcons, ars)  @  multi_arity_clause tc_arlists
   3.122 +fun multi_arity_clause dfg [] = []
   3.123 +  | multi_arity_clause dfg ((tcons,ars) :: tc_arlists) =
   3.124 +      arity_clause dfg [] 1 (tcons, ars)  @  multi_arity_clause dfg tc_arlists
   3.125  
   3.126  (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   3.127    provided its arguments have the corresponding sorts.*)
   3.128 @@ -390,10 +388,10 @@
   3.129            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   3.130        in  (classes' union classes, cpairs' union cpairs)  end;
   3.131  
   3.132 -fun make_arity_clauses thy tycons classes =
   3.133 +fun make_arity_clauses_dfg dfg thy tycons classes =
   3.134    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   3.135 -  in  (classes', multi_arity_clause cpairs)  end;
   3.136 -
   3.137 +  in  (classes', multi_arity_clause dfg cpairs)  end;
   3.138 +val make_arity_clauses = make_arity_clauses_dfg false;
   3.139  
   3.140  (**** Find occurrences of predicates in clauses ****)
   3.141  
     4.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Feb 25 10:02:10 2009 +0100
     4.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Feb 26 10:13:43 2009 +0100
     4.3 @@ -106,67 +106,68 @@
     4.4  
     4.5  fun isTaut (Clause {literals,...}) = exists isTrue literals;
     4.6  
     4.7 -fun type_of (Type (a, Ts)) =
     4.8 -      let val (folTypes,ts) = types_of Ts
     4.9 -      in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
    4.10 -  | type_of (tp as (TFree(a,s))) =
    4.11 +fun type_of dfg (Type (a, Ts)) =
    4.12 +      let val (folTypes,ts) = types_of dfg Ts
    4.13 +      in  (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts)  end
    4.14 +  | type_of dfg (tp as (TFree(a,s))) =
    4.15        (RC.AtomF (RC.make_fixed_type_var a), [tp])
    4.16 -  | type_of (tp as (TVar(v,s))) =
    4.17 +  | type_of dfg (tp as (TVar(v,s))) =
    4.18        (RC.AtomV (RC.make_schematic_type_var v), [tp])
    4.19 -and types_of Ts =
    4.20 -      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    4.21 +and types_of dfg Ts =
    4.22 +      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    4.23        in  (folTyps, RC.union_all ts)  end;
    4.24  
    4.25  (* same as above, but no gathering of sort information *)
    4.26 -fun simp_type_of (Type (a, Ts)) =
    4.27 -      RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
    4.28 -  | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
    4.29 -  | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
    4.30 +fun simp_type_of dfg (Type (a, Ts)) =
    4.31 +      RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    4.32 +  | simp_type_of dfg (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
    4.33 +  | simp_type_of dfg (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
    4.34  
    4.35  
    4.36 -fun const_type_of thy (c,t) =
    4.37 -      let val (tp,ts) = type_of t
    4.38 -      in  (tp, ts, map simp_type_of (Sign.const_typargs thy (c,t))) end;
    4.39 +fun const_type_of dfg thy (c,t) =
    4.40 +      let val (tp,ts) = type_of dfg t
    4.41 +      in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
    4.42  
    4.43  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    4.44 -fun combterm_of thy (Const(c,t)) =
    4.45 -      let val (tp,ts,tvar_list) = const_type_of thy (c,t)
    4.46 -          val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
    4.47 +fun combterm_of dfg thy (Const(c,t)) =
    4.48 +      let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
    4.49 +          val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
    4.50        in  (c',ts)  end
    4.51 -  | combterm_of thy (Free(v,t)) =
    4.52 -      let val (tp,ts) = type_of t
    4.53 +  | combterm_of dfg thy (Free(v,t)) =
    4.54 +      let val (tp,ts) = type_of dfg t
    4.55            val v' = CombConst(RC.make_fixed_var v, tp, [])
    4.56        in  (v',ts)  end
    4.57 -  | combterm_of thy (Var(v,t)) =
    4.58 -      let val (tp,ts) = type_of t
    4.59 +  | combterm_of dfg thy (Var(v,t)) =
    4.60 +      let val (tp,ts) = type_of dfg t
    4.61            val v' = CombVar(RC.make_schematic_var v,tp)
    4.62        in  (v',ts)  end
    4.63 -  | combterm_of thy (P $ Q) =
    4.64 -      let val (P',tsP) = combterm_of thy P
    4.65 -          val (Q',tsQ) = combterm_of thy Q
    4.66 +  | combterm_of dfg thy (P $ Q) =
    4.67 +      let val (P',tsP) = combterm_of dfg thy P
    4.68 +          val (Q',tsQ) = combterm_of dfg thy Q
    4.69        in  (CombApp(P',Q'), tsP union tsQ)  end
    4.70 -  | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
    4.71 +  | combterm_of _ thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
    4.72  
    4.73 -fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
    4.74 -  | predicate_of thy (t,polarity) = (combterm_of thy (Envir.eta_contract t), polarity);
    4.75 +fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
    4.76 +  | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
    4.77  
    4.78 -fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
    4.79 -  | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =
    4.80 -      literals_of_term1 thy (literals_of_term1 thy args P) Q
    4.81 -  | literals_of_term1 thy (lits,ts) P =
    4.82 -      let val ((pred,ts'),pol) = predicate_of thy (P,true)
    4.83 +fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
    4.84 +  | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
    4.85 +      literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
    4.86 +  | literals_of_term1 dfg thy (lits,ts) P =
    4.87 +      let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
    4.88        in
    4.89            (Literal(pol,pred)::lits, ts union ts')
    4.90        end;
    4.91  
    4.92 -fun literals_of_term thy P = literals_of_term1 thy ([],[]) P;
    4.93 +fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
    4.94 +val literals_of_term = literals_of_term_dfg false;
    4.95  
    4.96  (* Problem too trivial for resolution (empty clause) *)
    4.97  exception TOO_TRIVIAL;
    4.98  
    4.99  (* making axiom and conjecture clauses *)
   4.100 -fun make_clause thy (clause_id,axiom_name,kind,th) =
   4.101 -    let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
   4.102 +fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
   4.103 +    let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
   4.104      in
   4.105          if forall isFalse lits
   4.106          then raise TOO_TRIVIAL
   4.107 @@ -176,20 +177,20 @@
   4.108      end;
   4.109  
   4.110  
   4.111 -fun add_axiom_clause thy ((th,(name,id)), pairs) =
   4.112 -  let val cls = make_clause thy (id, name, RC.Axiom, th)
   4.113 +fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
   4.114 +  let val cls = make_clause dfg thy (id, name, RC.Axiom, th)
   4.115    in
   4.116        if isTaut cls then pairs else (name,cls)::pairs
   4.117    end;
   4.118  
   4.119 -fun make_axiom_clauses thy = foldl (add_axiom_clause thy) [];
   4.120 +fun make_axiom_clauses dfg thy = foldl (add_axiom_clause dfg thy) [];
   4.121  
   4.122 -fun make_conjecture_clauses_aux _ _ [] = []
   4.123 -  | make_conjecture_clauses_aux thy n (th::ths) =
   4.124 -      make_clause thy (n,"conjecture", RC.Conjecture, th) ::
   4.125 -      make_conjecture_clauses_aux thy (n+1) ths;
   4.126 +fun make_conjecture_clauses_aux dfg _ _ [] = []
   4.127 +  | make_conjecture_clauses_aux dfg thy n (th::ths) =
   4.128 +      make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
   4.129 +      make_conjecture_clauses_aux dfg thy (n+1) ths;
   4.130  
   4.131 -fun make_conjecture_clauses thy = make_conjecture_clauses_aux thy 0;
   4.132 +fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
   4.133  
   4.134  
   4.135  (**********************************************************************)
   4.136 @@ -398,7 +399,7 @@
   4.137  fun cnf_helper_thms thy =
   4.138    ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
   4.139  
   4.140 -fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
   4.141 +fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
   4.142    if isFO then []  (*first-order*)
   4.143    else
   4.144      let val ct0 = foldl count_clause init_counters conjectures
   4.145 @@ -415,7 +416,7 @@
   4.146                  else []
   4.147          val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
   4.148      in
   4.149 -        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
   4.150 +        map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
   4.151      end;
   4.152  
   4.153  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   4.154 @@ -462,10 +463,9 @@
   4.155  (* write TPTP format to a single file *)
   4.156  fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   4.157      let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
   4.158 -        val _ = RC.dfg_format := false
   4.159 -        val conjectures = make_conjecture_clauses thy thms
   4.160 -        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
   4.161 -        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
   4.162 +        val conjectures = make_conjecture_clauses false thy thms
   4.163 +        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses false thy ax_tuples)
   4.164 +        val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas)
   4.165          val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
   4.166          val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures)
   4.167          val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   4.168 @@ -486,10 +486,9 @@
   4.169  
   4.170  fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   4.171      let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
   4.172 -        val _ = RC.dfg_format := true
   4.173 -        val conjectures = make_conjecture_clauses thy thms
   4.174 -        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
   4.175 -        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
   4.176 +        val conjectures = make_conjecture_clauses true thy thms
   4.177 +        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses true thy ax_tuples)
   4.178 +        val helper_clauses = get_helper_clauses true thy isFO (conjectures, axclauses, user_lemmas)
   4.179          val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
   4.180          val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_min_arity const_needs_hBOOL) conjectures)
   4.181          and probname = Path.implode (Path.base (Path.explode filename))