diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Tue Mar 03 19:08:04 2015 +0100
@@ -88,8 +88,8 @@
   then o_alg ctxt P idx vs
          (map (fn (pv :: pats, thm) =>
            (pats, refl RS
-            (inst_free (cterm_of (Proof_Context.theory_of ctxt) pv)
-              (cterm_of (Proof_Context.theory_of ctxt) v) thm))) pts)
+            (inst_free (Proof_Context.cterm_of ctxt pv)
+              (Proof_Context.cterm_of ctxt v) thm))) pts)
   else (* Cons case *)
     let
       val thy = Proof_Context.theory_of ctxt