--- a/src/HOL/Tools/metis_tools.ML Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Sep 17 21:27:08 2008 +0200
@@ -368,7 +368,7 @@
end;
(* INFERENCE RULE: REFL *)
- val refl_x = cterm_of @{theory} (hd (term_vars (prop_of REFL_THM)));
+ val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM)));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fun refl_inf ctxt t =
@@ -472,14 +472,14 @@
fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
- val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal");
- val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal");
+ 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 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;
+ 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;
fun type_ext thy tms =
let val subs = ResAtp.tfree_classes_of_terms tms