src/HOL/Tools/Function/function_lib.ML

--- a/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Fri Mar 06 13:39:34 2015 +0100
@@ -105,7 +105,7 @@
    val ty = fastype_of t
  in
    Goal.prove_internal ctxt []
-     (Thm.cterm_of thy
+     (Proof_Context.cterm_of ctxt
        (Logic.mk_equals (t,
           if null is
           then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))