src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42361 23f352990944
parent 42353 7797efa897a1
child 42449 494e4ac5b0f8
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -188,7 +188,7 @@
   in aux (maxidx_of_term t + 1) t end
 
 fun introduce_combinators_in_term ctxt kind t =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     if Meson.is_fol_term thy t then
       t
     else
@@ -241,7 +241,7 @@
 (* making fact and conjecture formulas *)
 fun make_formula ctxt eq_as_iff presimp name kind t =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
               |> transform_elim_term
               |> Object_Logic.atomize_term thy
@@ -324,7 +324,7 @@
 
 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val fact_ts = map (prop_of o snd o snd) rich_facts
     val (facts, fact_names) =
       rich_facts
@@ -375,7 +375,7 @@
     is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
   | is_type_dangerous _ _ = false
 and is_type_constr_dangerous ctxt s =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     case Datatype_Data.get_info thy s of
       SOME {descr, ...} =>
       forall (fn (_, (_, _, constrs)) =>
@@ -444,7 +444,7 @@
 
 fun fo_term_for_combterm ctxt type_sys =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     fun aux top_level u =
       let
         val (head, args) = strip_combterm_comb u
@@ -681,7 +681,7 @@
 fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
                         explicit_apply hyp_ts concl_t facts =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt type_sys hyp_ts concl_t facts
     (* Reordering these might or might not confuse the proof reconstruction