--- a/src/HOL/Tools/metis_tools.ML Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Jul 15 23:48:21 2009 +0200
@@ -371,7 +371,7 @@
end;
(* INFERENCE RULE: REFL *)
- val refl_x = cterm_of (the_context ()) (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
+ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fun refl_inf ctxt t =
@@ -475,14 +475,14 @@
fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
- val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal");
- val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal");
+ val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
+ val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
- val comb_I = cnf_th (the_context ()) ResHolClause.comb_I;
- val comb_K = cnf_th (the_context ()) ResHolClause.comb_K;
- val comb_B = cnf_th (the_context ()) ResHolClause.comb_B;
- val comb_C = cnf_th (the_context ()) ResHolClause.comb_C;
- val comb_S = cnf_th (the_context ()) ResHolClause.comb_S;
+ val comb_I = cnf_th @{theory} ResHolClause.comb_I;
+ val comb_K = cnf_th @{theory} ResHolClause.comb_K;
+ val comb_B = cnf_th @{theory} ResHolClause.comb_B;
+ val comb_C = cnf_th @{theory} ResHolClause.comb_C;
+ val comb_S = cnf_th @{theory} ResHolClause.comb_S;
fun type_ext thy tms =
let val subs = ResAtp.tfree_classes_of_terms tms