--- a/src/HOL/Tools/res_axioms.ML Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Sep 17 21:27:08 2008 +0200
@@ -159,9 +159,9 @@
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
-val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_S}));
(*FIXME: requires more use of cterm constructors*)
fun abstract ct =