src/HOL/Tools/Function/scnp_reconstruct.ML

--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -272,7 +272,7 @@
     val level_mapping =
       map_index pt_lev lev
         |> Termination.mk_sumcases D (setT nat_pairT)
-        |> Proof_Context.cterm_of ctxt
+        |> Thm.cterm_of ctxt
     in
       PROFILE "Proof Reconstruction"
         (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1